fun inst_abs (Const sT) = Const sT  (*TODO.WN100907 drop thy*)

 fun inst_abs (Const sT) = Const sT

     let val b' = subst_bound (Free (v, T2), b);

     let val b' = subst_bound (Free (v, T2), b); (*fun variant_abs: term.ML*)

     (*fun variant_abs: term.ML*)

     if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT 

     if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])

     else Type (s, [])

     if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT 

     if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)

     else TFree (s, srt)

   | T_a2real (TVar (("DUMMY", _), _)) = HOLogic.realT

     if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT 

     if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TVar ((s, i), srt)

     else TVar ((s, i), srt)

   | T_a2real (TVar (("DUMMY",_), srt)) = HOLogic.realT;

 (*FIXME .. fixes the type (+see Typefix.thy*)

 (* TODO clarify parse with Test_Isac *)

 (* before 2002 *)

 fun parseold thy str = (* before 2002 *)

 fun parseold thy str = 

   (let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str)

   (let val t = ((*typ_a2real o*) numbers_to_string) 

 		   (Syntax.read_term_global thy str)

     handle _ => NONE;

   handle _(*EXN? ..Inner syntax error Failed to parse term*) => NONE;

 (*2002 fun parseN thy str = 

 fun parseN thy str = (* introduced 2002 *)

   (let 

   (let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)

      val sgn = sign_of thy;

      val t = ((*typ_a2real o app_num_tr'1 o*) term_of) 

        (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));

    in SOME (Thm.global_cterm_of sgn t) end)

      handle _ => NONE;*)

 fun parseN thy str = 

   (let val t = (*(typ_a2real o numbers_to_string)*) 

 	   (Syntax.read_term_global thy str)

     handle _ => NONE;

   handle _(*EXN? ..Inner syntax error Failed to parse term*) => NONE;

 (*2002 fun parse thy str = 

 fun parse thy str = (* introduced 2010 *)

   (let 

   (let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)

      val sgn = sign_of thy;

    in SOME (Thm.global_cterm_of thy t) end)

      val t = (typ_a2real o app_num_tr'1 o Thm.term_of) 

   handle _(*EXN? ..Inner syntax error Failed to parse term*) => NONE;

        (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));

    in SOME (Thm.global_cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)

      handle _ => NONE;*)

 (*2010 fun parse thy str = 

   (let val t = (typ_a2real o app_num_tr'1) (Syntax.read_term_global thy str)

    in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)

      handle _ => NONE;*)

 fun parse thy str = 

   (let val t = (typ_a2real o numbers_to_string) 

 		   (Syntax.read_term_global thy str)

    in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)

      handle _ => NONE;

 (*

 > val (SOME ct) = parse thy "(-#5)^^^#3"; 

 > atomty (Thm.term_of ct);

 *** -------------

 *** Const ( Nat.op ^, ['a, nat] => 'a)

 ***   Const ( uminus, 'a => 'a)

 ***     Free ( #5, 'a)

 ***   Free ( #3, nat)                

 > val (SOME ct) = parse thy "R=R"; 

 > atomty (Thm.term_of ct);

 *** -------------

 *** Const ( op =, [real, real] => bool)

 ***   Free ( R, real)

 ***   Free ( R, real)

 THIS IS THE OUTPUT FOR VERSION (3) above at typ_a2real !!!!!

 *** -------------

 *** Const ( op =, [RealDef.real, RealDef.real] => bool)

 ***   Free ( R, RealDef.real)

 ***   Free ( R, RealDef.real)                  *)

       handle _ => NONE;

    handle _ => NONE;

 fun parse_patt thy str = (thy, str) |>> thy2ctxt 

 fun parse_patt thy str =

                                     |-> Proof_Context.read_term_pattern

   (thy, str) |>> thy2ctxt 

                                     |> numbers_to_string (*TODO drop*)

              |-> Proof_Context.read_term_pattern

                                     |> typ_a2real;       (*TODO drop*)

              |> numbers_to_string (*TODO drop*)

              |> typ_a2real;       (*TODO drop*)

 (*version for testing local to theories*)

 fun str2term_ thy str = (Thm.term_of o the o (parse thy)) str;

 (*WN110520

 fun str2term str = (Thm.term_of o the o (parse (Thy_Info_get_theory "Isac"))) str;*)

 fun strs2terms ss = map str2term ss;

 fun str2termN str = (Thm.term_of o the o (parseN (Thy_Info_get_theory "Isac"))) str;

 (* TODO decide with Test_Isac *)

 fun is_atom t = length (vars t) = 1

 (*+ makes a substitution from the output of Pattern.match +*)

 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)

 fun mk_subs (subs: ((string * int) * (Term.typ * Term.term)) list) =

 let fun mk_sub ((id, _), (ty, tm)) = (Free (id, ty), tm) in

 map mk_sub subs end;

 val atomthm = atomt o #prop o Thm.rep_thm;

 (*.instantiate #prop thm with bound variables (as Free).*)

 fun inst_bdv [] t = t : term

   | inst_bdv (instl: (term*term) list) t =

       let fun subst (v as Var((s,_),T)) = 

 	      (case Symbol.explode s of

 		   "b"::"d"::"v"::_ => 

 		   if_none (assoc(instl,Free(s,T))) (Free(s,T))

 		 | _ => v)

             | subst (Abs(a,T,body)) = Abs(a, T, subst body)

             | subst (f$t') = subst f $ subst t'

             | subst t = if_none (assoc(instl,t)) t

       in  subst t  end;

 (*WN050829 caution: is_atom (str2term"q_0/2 * L * x") = true !!!

   use length (vars term) = 1 instead*)

 (* val t = str2term "q_0/2 * L * x";

 (* from Pure/term.ML; reports if ALL Free's have found a substitution

    (required for evaluating the preconditions of _incomplete_ models) *)

 *)

 fun subst_atomic_all [] t = (false (*TODO may be 'true' for some terms ?*), t)

 (*val t = str2term "Float ((1,2),(0,0))";

   | subst_atomic_all instl t =

 > is_atom t;

     let

 val it = true : bool

       fun subst (Abs (a, T, body)) = 

 > val t = str2term "Float ((1,2),(0,0)) * I__";

           let

 > is_atom t;

             val (all, body') = subst body

 val it = true : bool

           in (all, Abs(a, T, body')) end

 > val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";

         | subst (f$tt) = 

 > is_atom t;

 	        let

 val it = true : bool

 	          val (all1, f') = subst f

 > val t = str2term "1 + 2*I__";

 	          val (all2, tt') = subst tt

 > val Const ("Groups.plus_class.plus",_) $ t1 $ (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_)) = t;

 	        in (all1 andalso all2, f' $ tt') end

 *)

         | subst (t as Free _) = 

 	        if is_num t then (true, t) (*numerals cannot be subst*)

 (*.adaption from Isabelle/src/Pure/term.ML; reports if ALL Free's

 	        else (case assoc (instl, t) of

    have found a substitution (required for evaluating the preconditions

 					  SOME t' => (true, t')

    of _incomplete_ models).*)

 				  | NONE => (false, t))

 fun subst_atomic_all [] t = (false, (*TODO may be 'true' for some terms ?*)

         | subst t = (true, if_none (assoc(instl,t)) t)

 			     t : term)

     in subst t end;

   | subst_atomic_all (instl: (term*term) list) t =

       let fun subst (Abs(a,T,body)) = 

 	      let val (all, body') = subst body

 	      in (all, Abs(a, T, body')) end

             | subst (f$tt) = 

 	      let val (all1, f') = subst f

 		  val (all2, tt') = subst tt

 	      in (all1 andalso all2, f' $ tt') end

             | subst (t as Free _) = 

 	      if is_num t then (true, t) (*numerals cannot be subst*)

 	      else (case assoc(instl,t) of

 					 SOME t' => (true, t')

 				       | NONE => (false, t))

             | subst t = (true, if_none (assoc(instl,t)) t)

       in  subst t  end;