lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
--- 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);
(*
--- 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 :
--- 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)
--- 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
--- 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