# HG changeset patch # User dixon # Date 1115081155 -7200 # Node ID b0e8b37642a4f9cd283fc5495560b7b58167fe92 # Parent 2a8f8668574540b2e5b4723b8ace981309b54248 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments. diff -r 2a8f86685745 -r b0e8b37642a4 src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Tue May 03 02:44:10 2005 +0200 +++ b/src/Provers/eqsubst.ML Tue May 03 02:45:55 2005 +0200 @@ -28,8 +28,8 @@ sig type match = - ((Term.indexname * Term.typ) list (* type instantiations *) - * (Term.indexname * Term.term) list) (* term instantiations *) + ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *) + * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *) * (string * Term.typ) list (* fake named type abs env *) * (string * Term.typ) list (* type abs env *) * Term.term (* outer term *) @@ -122,13 +122,13 @@ : EQSUBST_TAC = struct - (* a type abriviation for match infomration *) + (* a type abriviation for match information *) type match = - ((Term.indexname * Term.typ) list (* type instantiations *) - * (Term.indexname * Term.term) list) (* term instantiations *) - * (string * Term.typ) list (* fake named type abs env *) - * (string * Term.typ) list (* type abs env *) - * Term.term (* outer term *) + ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *) + * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *) + * (string * Term.typ) list (* fake named type abs env *) + * (string * Term.typ) list (* type abs env *) + * Term.term (* outer term *) (* FOR DEBUGGING... @@ -209,7 +209,7 @@ fun apply_subst_in_concl i th (cfvs, conclthm) rule m = (RWInst.rw m rule conclthm) |> IsaND.unfix_frees cfvs - |> RWInst.beta_eta_contract_tac + |> RWInst.beta_eta_contract |> (fn r => Tactic.rtac r i th); (* @@ -281,7 +281,7 @@ (RWInst.rw m rule pth) |> Thm.permute_prems 0 ~1 |> IsaND.unfix_frees cfvs - |> RWInst.beta_eta_contract_tac + |> RWInst.beta_eta_contract |> (fn r => Tactic.dtac r i th); (* diff -r 2a8f86685745 -r b0e8b37642a4 src/Pure/IsaPlanner/isa_fterm.ML --- a/src/Pure/IsaPlanner/isa_fterm.ML Tue May 03 02:44:10 2005 +0200 +++ b/src/Pure/IsaPlanner/isa_fterm.ML Tue May 03 02:45:55 2005 +0200 @@ -34,8 +34,11 @@ Term.term -> FcTerm -> ( - ((Term.indexname * Term.typ) list * (Term.indexname * Term.term) list) - * (string * Term.typ) list * (string * Term.typ) list * Term.term) + ((Term.indexname * (Term.sort * Term.typ)) list + * (Term.indexname * (Term.typ * Term.term)) list) + * (string * Term.typ) list + * (string * Term.typ) list + * Term.term) option val clean_unify_ft : Sign.sg -> @@ -43,7 +46,8 @@ Term.term -> FcTerm -> ( - ((Term.indexname * Term.typ) list * (Term.indexname * Term.term) list) + ((Term.indexname * (Term.sort * Term.typ)) list + * (Term.indexname * (Term.typ * Term.term)) list) * (string * Term.typ) list * (string * Term.typ) list * Term.term) Seq.seq val enc_appl : diff -r 2a8f86685745 -r b0e8b37642a4 src/Pure/IsaPlanner/isand.ML --- a/src/Pure/IsaPlanner/isand.ML Tue May 03 02:44:10 2005 +0200 +++ b/src/Pure/IsaPlanner/isand.ML Tue May 03 02:45:55 2005 +0200 @@ -54,14 +54,26 @@ (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list val allify_conditions' : (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list + val assume_allified : + Sign.sg -> (string * Term.typ) list * (string * Term.sort) list + -> Term.term -> (Thm.cterm * Thm.thm) (* meta level fixed params (i.e. !! vars) *) + val fix_alls_in_term : Term.term -> Term.term * Term.term list val fix_alls_term : int -> Term.term -> Term.term * Term.term list val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list val fix_alls : int -> Thm.thm -> Thm.thm * export (* meta variables in types and terms *) + val fix_tvars_to_tfrees_in_terms + : string list (* avoid these names *) + -> Term.term list -> + (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *) + val fix_vars_to_frees_in_terms + : string list (* avoid these names *) + -> Term.term list -> + (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *) val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm val fix_vars_and_tvars : @@ -144,60 +156,89 @@ fun allify_conditions' Ts th = allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th; - +(* allify types *) +fun allify_typ ts ty = + let + fun trec (x as (TFree (s,srt))) = + (case Library.find_first (fn (s2,srt2) => s = s2) ts + of NONE => x + | SOME (s2,_) => TVar ((s,0),srt)) + (* Maybe add in check here for bad sorts? + if srt = srt2 then TVar ((s,0),srt) + else raise ("thaw_typ", ts, ty) *) + | trec (Type (s,typs)) = Type (s, map trec typs) + | trec (v as TVar _) = v; + in trec ty end; -(* These should be defined in term.ML *) -fun dest_TVar (TVar x) = x - | dest_TVar T = raise TYPE ("dest_TVar", [T], []); -fun dest_TFree (TFree x) = x - | dest_TFree T = raise TYPE ("dest_TFree", [T], []); +(* implicit typ's and term *) +val allify_term_typs = Term.map_term_types o allify_typ; +(* allified version of term, given frees and types to allify over *) +fun assume_allified sgn (vs,tyvs) t = + let + fun allify_var (vt as (n,ty),t) = + (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) + fun allify Ts p = List.foldr allify_var p Ts + + val ctermify = Thm.cterm_of sgn; + val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs + val allified_term = t |> allify vs; + val ct = ctermify allified_term; + val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term); + in (typ_allified_ct, + Drule.forall_elim_vars 0 (Thm.assume ct)) end; (* change type-vars to fresh type frees *) -fun fix_tvars_to_tfrees th = +fun fix_tvars_to_tfrees_in_terms names ts = let - val sign = Thm.sign_of_thm th - val ctermify = Thm.cterm_of sign - val ctypify = Thm.ctyp_of sign - - val prop = Thm.prop_of th; - val tfree_names = map fst (Term.add_term_tfrees (prop,[])); - val tvars = Term.add_term_tvars (prop, []); - + val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts); + val tvars = List.foldr Term.add_term_tvars [] ts; val (names',renamings) = List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => let val n2 = Term.variant Ns n in - (n2::Ns, (ctypify (TVar tv), - ctypify (TFree (n2,s)))::Rs) - end) (tfree_names,[]) tvars; + (n2::Ns, (tv, (n2,s))::Rs) + end) (tfree_names @ names,[]) tvars; + in renamings end; +fun fix_tvars_to_tfrees th = + let + val sign = Thm.sign_of_thm th; + val ctypify = Thm.ctyp_of sign; + val renamings = fix_tvars_to_tfrees_in_terms [] [Thm.prop_of th]; + val crenamings = + map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f))) + renamings; + val fixedfrees = map snd crenamings; + in (fixedfrees, Thm.instantiate (crenamings, []) th) end; - val fixedfrees = map snd renamings; - in - (fixedfrees, Thm.instantiate (renamings, []) th) - end; (* change type-free's to type-vars *) fun unfix_tfrees ns th = - fst (Thm.varifyT' (map (fn x => dest_TFree (Thm.typ_of x)) ns) th); + let + val varfiytfrees = (map (fn x => Term.dest_TFree (Thm.typ_of x)) ns) + val skiptfrees = Term.add_term_tfrees (Thm.prop_of th,[]) \\ varfiytfrees; + in fst (Thm.varifyT' skiptfrees th) end; -(* change schematic vars to fresh free vars *) +(* change schematic/meta vars to fresh free vars *) +fun fix_vars_to_frees_in_terms names ts = + let + val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts); + val Ns = List.foldr Term.add_term_names names ts; + val (_,renamings) = + Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => + let val n2 = Term.variant Ns n in + (n2 :: Ns, (v, (n2,ty)) :: Rs) + end) ((Ns,[]), vars); + in renamings end; fun fix_vars_to_frees th = let val ctermify = Thm.cterm_of (Thm.sign_of_thm th) - val prop = Thm.prop_of th - val vars = map Term.dest_Var (Term.term_vars prop) - - val names = Term.add_term_names (prop, []) + val renamings = fix_vars_to_frees_in_terms [] [Thm.prop_of th]; + val crenamings = + map (fn (v,f) => (ctermify (Var v), ctermify (Free f))) + renamings; + val fixedfrees = map snd crenamings; + in (fixedfrees, Thm.instantiate ([], crenamings) th) end; - val (insts,names2) = - Library.foldl (fn ((insts,names),v as ((n,i),ty)) => - let val n2 = Term.variant names n in - ((ctermify (Var v), ctermify (Free(n2,ty))) :: insts, - n2 :: names) - end) - (([],names), vars) - val fixedfrees = map snd insts; - in (fixedfrees, Thm.instantiate ([], insts) th) end; (* make free vars into schematic vars with index zero *) fun unfix_frees frees = @@ -333,8 +374,11 @@ Note, an advantage of this over Isar is that it supports instantiation of unkowns in the earlier theorem, ie we can do instantiation of meta -vars! *) -(* loosely corresponds to: +vars! + +avoids constant, free and vars names. + +loosely corresponds to: Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm Result: ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, @@ -342,9 +386,21 @@ ("As ==> SGi x'" : thm) -> ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) *) +fun fix_alls_in_term alledt = + let + val t = Term.strip_all_body alledt; + val alls = rev (Term.strip_all_vars alledt); + val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) + val names = Term.add_term_names (t,varnames); + val fvs = map Free + ((Term.variantlist (map fst alls, names)) + ~~ (map snd alls)); + in ((subst_bounds (fvs,t)), fvs) end; + fun fix_alls_term i t = let - val names = Term.add_term_names (t,[]); + val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t) + val names = Term.add_term_names (t,varnames); val gt = Logic.get_goal t i; val body = Term.strip_all_body gt; val alls = rev (Term.strip_all_vars gt); @@ -407,13 +463,14 @@ back a new goal thm and an exporter, the new goalthm is as the old one, but without the premices, and the exporter will use a proof of the new goalthm, possibly using the assumed premices, to shoe the -orginial goal. *) +orginial goal. -(* Note: Dealing with meta vars, need to meta-level-all them in the +Note: Dealing with meta vars, need to meta-level-all them in the shyps, which we can later instantiate with a specific value.... ? think about this... maybe need to introduce some new fixed vars and -then remove them again at the end... like I do with rw_inst. *) -(* loosely corresponds to: +then remove them again at the end... like I do with rw_inst. + +loosely corresponds to: Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm Result: (["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions @@ -508,14 +565,8 @@ *) fun hide_prems th = let - val sgn = Thm.sign_of_thm th; - val ctermify = Thm.cterm_of sgn; - - val t = (prop_of th); - val prems = Logic.strip_imp_prems t; - val cprems = map ctermify prems; - val aprems = map Thm.trivial cprems; - + val cprems = Drule.cprems_of th; + val aprems = map Thm.assume cprems; (* val unhidef = Drule.implies_intr_list cprems; *) in (Drule.implies_elim_list th aprems, cprems) diff -r 2a8f86685745 -r b0e8b37642a4 src/Pure/IsaPlanner/rw_inst.ML --- a/src/Pure/IsaPlanner/rw_inst.ML Tue May 03 02:44:10 2005 +0200 +++ b/src/Pure/IsaPlanner/rw_inst.ML Tue May 03 02:45:55 2005 +0200 @@ -18,8 +18,8 @@ (* Rewrite: give it instantiation infromation, a rule, and the target thm, and it will return the rewritten target thm *) val rw : - ((Term.indexname * Term.typ) list * (* type var instantiations *) - (Term.indexname * Term.term) list) (* schematic var instantiations *) + ((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *) + (Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *) * (string * Term.typ) list (* Fake named bounds + types *) * (string * Term.typ) list (* names of bound + types *) * Term.term -> (* outer term for instantiation *) @@ -35,32 +35,36 @@ -> (string * Term.typ) list (* hopeful name of outer bounds *) -> Thm.thm -> Thm.cterm list * Thm.thm val mk_fixtvar_tyinsts : - Term.indexname list -> - Term.term list -> ((string * int) * Term.typ) list * (string * sort) list + (Term.indexname * (Term.sort * Term.typ)) list -> + Term.term list -> ((string * int) * (Term.sort * Term.typ)) list + * (string * Term.sort) list val mk_renamings : Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list val new_tfree : ((string * int) * Term.sort) * - (((string * int) * Term.typ) list * string list) -> - ((string * int) * Term.typ) list * string list - val cross_inst : (Term.indexname * Term.term) list - -> (Term.indexname * Term.term) list + (((string * int) * (Term.sort * Term.typ)) list * string list) -> + ((string * int) * (Term.sort * Term.typ)) list * string list + val cross_inst : (Term.indexname * (Term.typ * Term.term)) list + -> (Term.indexname *(Term.typ * Term.term)) list + val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list + -> (Term.indexname * (Term.sort * Term.typ)) list - val beta_contract_tac : Thm.thm -> Thm.thm - val beta_eta_contract_tac : Thm.thm -> Thm.thm + val beta_contract : Thm.thm -> Thm.thm + val beta_eta_contract : Thm.thm -> Thm.thm end; -structure RWInst : RW_INST= -struct +structure RWInst +(* : RW_INST *) += struct (* beta contract the theorem *) -fun beta_contract_tac thm = +fun beta_contract thm = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; (* beta-eta contract the theorem *) -fun beta_eta_contract_tac thm = +fun beta_eta_contract thm = let val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 @@ -149,18 +153,21 @@ (* make a new fresh typefree instantiation for the given tvar *) fun new_tfree (tv as (ix,sort), (pairs,used)) = let val v = variant used (string_of_indexname ix) - in ((ix,TFree(v,sort))::pairs, v::used) end; + in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; (* make instantiations to fix type variables that are not already instantiated (in ignore_ixs) from the list of terms. *) -fun mk_fixtvar_tyinsts ignore_ixs ts = - let val (tvars, tfrees) = +fun mk_fixtvar_tyinsts ignore_insts ts = + let + val ignore_ixs = map fst ignore_insts; + val (tvars, tfrees) = foldr (fn (t, (varixs, tfrees)) => (Term.add_term_tvars (t,varixs), Term.add_term_tfrees (t,tfrees))) ([],[]) ts; - val unfixed_tvars = List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars; + val unfixed_tvars = + List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars; val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars in (fixtyinsts, tfrees) end; @@ -170,19 +177,22 @@ and thus only one-parsing of the instantiations is necessary. *) fun cross_inst insts = let - fun instL (ix, t) = - map (fn (ix2,t2) => (ix2, Term.subst_vars ([], [(ix, t)]) t2)); + fun instL (ix, (ty,t)) = + map (fn (ix2,(ty2,t2)) => + (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); fun cross_instL ([], l) = rev l | cross_instL ((ix, t) :: insts, l) = cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); in cross_instL (insts, []) end; + (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) fun cross_inst_typs insts = let - fun instL (ix, ty) = - map (fn (ix2,ty2) => (ix2, Term.typ_subst_TVars [(ix, ty)] ty2)); + fun instL (ix, (srt,ty)) = + map (fn (ix2,(srt2,ty2)) => + (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); fun cross_instL ([], l) = rev l | cross_instL ((ix, t) :: insts, l) = @@ -207,30 +217,27 @@ (* fix all non-instantiated tvars *) val (fixtyinsts, othertfrees) = - mk_fixtvar_tyinsts (map fst nonfixed_typinsts) + mk_fixtvar_tyinsts nonfixed_typinsts [Thm.prop_of rule, Thm.prop_of target_thm]; - + val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) - val ctyp_insts = map (apsnd ctypeify) typinsts; + val ctyp_insts = + map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) typinsts; (* type instantiated versions *) - fun tyinst insts rule = - let val (_, rsorts) = types_sorts rule - in Thm.instantiate (List.mapPartial (fn (ixn, cT) => Option.map - (fn S => (ctypeify (TVar (ixn, S)), cT)) (rsorts ixn)) insts, []) rule - end; - val tgt_th_tyinst = tyinst ctyp_insts target_thm; - val rule_tyinst = tyinst ctyp_insts rule; + val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; + val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; + val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts; (* type instanitated outer term *) - val outerterm_tyinst = - Term.subst_vars (typinsts,[]) outerterm; + val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; (* type-instantiate the var instantiations *) - val insts_tyinst = foldr (fn ((ix,t),insts_tyinst) => - (ix, Term.subst_vars (typinsts,[]) t) + val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => + (ix, (Term.typ_subst_TVars term_typ_inst ty, + Term.subst_TVars term_typ_inst t)) :: insts_tyinst) [] unprepinsts; @@ -239,8 +246,8 @@ (* create certms of instantiations *) val cinsts_tyinst = - map (fn (ix,t) => (ctermify (Var (ix, Term.type_of t)), - ctermify t)) insts_tyinst_inst; + map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), + ctermify t)) insts_tyinst_inst; (* The instantiated rule *) val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); @@ -256,15 +263,14 @@ (* Create the specific version of the rule for this target application *) val outerterm_inst = outerterm_tyinst - |> Term.subst_vars ([], insts_tyinst_inst) - |> Term.subst_vars ([], map (fn ((ix,ty),t) => (ix,t)) - renamings); + |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst) + |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings); val couter_inst = Thm.reflexive (ctermify outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst |> Thm.instantiate ([], cterm_renamings) |> mk_abstractedrule FakeTs Ts; val specific_tgt_rule = - beta_eta_contract_tac + beta_eta_contract (Thm.combination couter_inst abstract_rule_inst); (* create an instantiated version of the target thm *) @@ -275,7 +281,7 @@ val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; in - (beta_eta_contract_tac tgt_th_inst) + (beta_eta_contract tgt_th_inst) |> Thm.equal_elim specific_tgt_rule |> Drule.implies_intr_list cprems |> Drule.forall_intr_list frees_of_fixed_vars diff -r 2a8f86685745 -r b0e8b37642a4 src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Tue May 03 02:44:10 2005 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Tue May 03 02:45:55 2005 +0200 @@ -22,11 +22,11 @@ (* Matching/unification with exceptions handled *) val clean_match : Type.tsig -> Term.term * Term.term - -> ((Term.indexname * Term.typ) list - * (Term.indexname * Term.term) list) option + -> ((Term.indexname * (Term.sort * Term.typ)) list + * (Term.indexname * (Term.typ * Term.term)) list) option val clean_unify : Sign.sg -> int -> Term.term * Term.term - -> ((Term.indexname * Term.typ) list - * (Term.indexname * Term.term) list) Seq.seq + -> ((Term.indexname * (Term.sort * Term.typ)) list + * (Term.indexname * (Term.typ * Term.term)) list) Seq.seq (* managing variables in terms, can doing conversions *) val bounds_to_frees : Term.term -> Term.term @@ -151,8 +151,7 @@ (* returns optional instantiation *) fun clean_match tsig (a as (pat, t)) = let val (tyenv, tenv) = Pattern.match tsig a - in SOME (map (apsnd snd) (Vartab.dest tyenv), - map (apsnd snd) (Vartab.dest tenv)) + in SOME (Vartab.dest tyenv, Vartab.dest tenv) end handle Pattern.MATCH => NONE; (* Higher order unification with exception handled, return the instantiations *) (* given Signature, max var index, pat, tgt *) @@ -176,8 +175,8 @@ (* is it right to throw away the flexes? or should I be using them somehow? *) fun mk_insts (env,flexflexes) = - (map (apsnd snd) (Vartab.dest (Envir.type_env env)), - map (apsnd snd) (Envir.alist_of env)); + (Vartab.dest (Envir.type_env env), + Envir.alist_of env); val initenv = Envir.Envir {asol = Vartab.empty, iTs = typinsttab, maxidx = ix2}; val useq = (Unify.unifiers (sgn,initenv,[a])) @@ -265,8 +264,8 @@ (* functions *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -fun current_sign () = sign_of (the_context()); -fun cterm_of_term (t : term) = cterm_of (current_sign()) t; +fun current_sign () = Theory.sign_of (the_context()); +fun cterm_of_term (t : term) = Thm.cterm_of (current_sign()) t; fun term_of_thm t = (Thm.prop_of t); (* little function to make a trueprop of anything by putting a P