1.1 --- a/src/Tools/isac/ProgLang/termC.sml	Tue Jun 11 09:06:29 2013 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Fri Jun 14 15:46:09 2013 +0200
     1.3 @@ -1084,7 +1084,9 @@
     1.4  fun parseNEW ctxt str = SOME (Syntax.read_term ctxt str |> numbers_to_string)
     1.5        handle _ => NONE;
     1.6  
     1.7 -(* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation*)
     1.8 +(* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
     1.9 +  WN130613 probably compare to 
    1.10 +  http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
    1.11  fun parse_patt thy str = (thy, str) |>> thy2ctxt 
    1.12                                      |-> Proof_Context.read_term_pattern
    1.13                                      |> numbers_to_string (*TODO drop*)

     2.1 --- a/test/Tools/isac/Test_Some2.thy	Tue Jun 11 09:06:29 2013 +0200
     2.2 +++ b/test/Tools/isac/Test_Some2.thy	Fri Jun 14 15:46:09 2013 +0200
     2.3 @@ -1,11 +1,27 @@
     2.4  
     2.5  theory Test_Some2
     2.6  imports "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly"
     2.7 -        "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_FP"
     2.8  begin
     2.9  ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly.sml"
    2.10  
    2.11  ML {*
    2.12 +(*http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
    2.13 +fun pat_to_term ctxt t =
    2.14 +  let
    2.15 +     fun new_var vs T = case Variable.variant_frees ctxt vs [("x", T)] of
    2.16 +                            v::_ => (Free v :: vs, Free v);
    2.17 +     fun go (v as Var (_,T)) (vs,assocs) =
    2.18 +            (case AList.lookup op= assocs v of
    2.19 +               NONE => (case new_var vs T of
    2.20 +                   (vs', v') => (vs', (v,v') :: assocs))
    2.21 +               | _ => (vs,assocs))
    2.22 +        | go _ (vs,assocs) = (vs,assocs);
    2.23 +      val assocs = snd (Term.fold_aterms go t 
    2.24 +                       (map Free (Term.add_frees t []), []));
    2.25 +  in fst (yield_singleton (Variable.import_terms true) 
    2.26 +         (subst_atomic assocs t) ctxt)
    2.27 +  end;
    2.28 +
    2.29  *} 
    2.30  ML {*
    2.31  *}