[isabelle-dev] produce term patterns

[Walther Neuper]

Hope there is somebody who needs not dig in the code to answer this 
question ...

How can we produce specific patterns (some variables of a term should 
become Free, some Var), for instance:

(term_of o the o (parse thy)) "matches (?a + ?b * bdv^2 = (0::real)) equ";
val it =
    Const ("Tools.matches", "[bool, bool] =>  bool") $
          (Const ("op =", "[RealDef.real, RealDef.real] =>  bool") $
                (Const
                         ("op +",
                            "[RealDef.real, RealDef.real] =>  RealDef.real") $
                      Var (("a", 0), "RealDef.real") $
                   (Const
                            ("op *",
                               "[RealDef.real, RealDef.real] =>  RealDef.real")
                         $ Var (("b", 0), "RealDef.real") $
                      (Const
                               ("Nat.power",
                                  "[RealDef.real, nat] =>  RealDef.real") $
                            Free ("bdv", "RealDef.real") $
                         Free ("2", "nat")))) $ Free ("0", "RealDef.real")) $
       Free ("equ", "bool") : Term.term

The above is from an outdated Isabelle version --- what are the 
recommendations to produce specific patterns nowadays ?

Walther