--- a/src/Pure/Isar/rule_insts.ML Sat Apr 14 17:36:07 2007 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sat Apr 14 17:36:09 2007 +0200
@@ -21,7 +21,7 @@
fun is_tvar (x, _) = String.isPrefix "'" x;
-fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
+fun error_var msg xi = error (msg ^ Term.string_of_vname xi);
fun the_sort tvars xi = the (AList.lookup (op =) tvars xi)
handle Option.Option => error_var "No such type variable in theorem: " xi;
@@ -235,15 +235,14 @@
val (types, sorts) = types_sorts st;
(* Process type insts: Tinsts_env *)
fun absent xi = error
- ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
+ ("No such variable in theorem: " ^ Term.string_of_vname xi);
val (rtypes, rsorts) = types_sorts thm;
fun readT (xi, s) =
let val S = case rsorts xi of SOME S => S | NONE => absent xi;
- val T = Sign.read_typ (thy, sorts) s;
+ val T = Sign.read_def_typ (thy, sorts) s;
val U = TVar (xi, S);
in if Sign.typ_instance thy (T, U) then (U, T)
- else error
- ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
+ else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
end;
val Tinsts_env = map readT Tinsts;
(* Preprocess rule: extract vars and their types, apply Tinsts *)
--- a/src/Pure/drule.ML Sat Apr 14 17:36:07 2007 +0200
+++ b/src/Pure/drule.ML Sat Apr 14 17:36:09 2007 +0200
@@ -253,10 +253,10 @@
(** reading of instantiations **)
fun absent ixn =
- error("No such variable in term: " ^ Syntax.string_of_vname ixn);
+ error("No such variable in term: " ^ Term.string_of_vname ixn);
fun inst_failure ixn =
- error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
+ error("Instantiation of " ^ Term.string_of_vname ixn ^ " fails");
fun read_insts thy (rtypes,rsorts) (types,sorts) used insts =
let
@@ -266,7 +266,7 @@
fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
fun readT (ixn, st) =
let val S = sort_of ixn;
- val T = Sign.read_typ (thy,sorts) st;
+ val T = Sign.read_def_typ (thy,sorts) st;
in if Sign.typ_instance thy (T, TVar(ixn,S)) then (ixn,T)
else inst_failure ixn
end
@@ -277,7 +277,7 @@
val ixnsTs = map mkty vs;
val ixns = map fst ixnsTs
and sTs = map snd ixnsTs
- val (cts,tye2) = read_def_cterms(thy,types,sorts) used false sTs;
+ val (cts,tye2) = Thm.read_def_cterms(thy,types,sorts) used false sTs;
fun mkcVar(ixn,T) =
let val U = typ_subst_TVars tye2 T
in cterm_of thy (Var(ixn,U)) end
@@ -573,7 +573,7 @@
(*** Meta-Rewriting Rules ***)
-fun read_prop s = read_cterm ProtoPure.thy (s, propT);
+fun read_prop s = Thm.read_cterm ProtoPure.thy (s, propT);
fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
fun store_standard_thm name thm = store_thm name (standard thm);