--- a/src/FOLP/simp.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/FOLP/simp.ML Sat Apr 14 17:35:52 2007 +0200
@@ -591,13 +591,14 @@
fun mk_congs thy = List.concat o map (mk_cong_thy thy);
fun mk_typed_congs thy =
-let val S0 = Sign.defaultS thy;
- fun readfT(f,s) =
- let val T = Logic.incr_tvar 9 (Sign.read_typ(thy, K(SOME(S0))) s);
- val t = case Sign.const_type thy f of
- SOME(_) => Const(f,T) | NONE => Free(f,T)
- in (t,T) end
+let
+ fun readfT(f,s) =
+ let
+ val T = Logic.incr_tvar 9 (Sign.read_typ thy s);
+ val t = case Sign.const_type thy f of
+ SOME(_) => Const(f,T) | NONE => Free(f,T)
+ in (t,T) end
in List.concat o map (mk_cong_type thy o readfT) end;
-end (* local *)
-end (* SIMP *);
+end;
+end;
--- a/src/HOL/Import/import_syntax.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML Sat Apr 14 17:35:52 2007 +0200
@@ -137,7 +137,7 @@
val thyname = get_import_thy thy
in
Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp thy ty)) thy) (thy,constmaps)
+ | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Sign.read_typ thy ty) thy) (thy,constmaps)
end)
val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
@@ -147,7 +147,7 @@
val thyname = get_import_thy thy
in
Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp thy ty)) thy) (thy,constmaps)
+ | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Sign.read_typ thy ty) thy) (thy,constmaps)
end)
fun import_thy s =
--- a/src/HOL/Import/proof_kernel.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sat Apr 14 17:35:52 2007 +0200
@@ -225,7 +225,7 @@
fun F n =
let
val str = Library.setmp show_brackets false (G n string_of_cterm) ct
- val cu = read_cterm thy (str,T)
+ val cu = Thm.read_cterm thy (str,T)
in
if match cu
then quote str
@@ -473,10 +473,10 @@
val check_name_thy = theory "Main"
fun valid_boundvarname s =
- can (fn () => read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
+ can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
fun valid_varname s =
- can (fn () => read_cterm check_name_thy (s, TypeInfer.logicT)) ();
+ can (fn () => Thm.read_cterm check_name_thy (s, TypeInfer.logicT)) ();
fun protect_varname s =
if innocent_varname s andalso valid_varname s then s else
--- a/src/HOL/Library/sct.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Library/sct.ML Sat Apr 14 17:35:52 2007 +0200
@@ -4,13 +4,13 @@
Tactics for size change termination.
*)
-signature SCT =
+signature SCT =
sig
val abs_rel_tac : tactic
val mk_call_graph : tactic
end
-structure Sct : SCT =
+structure Sct : SCT =
struct
fun matrix [] ys = []
@@ -18,8 +18,8 @@
fun map_matrix f xss = map (map f) xss
-val scgT = Sign.read_typ (the_context (), K NONE) "scg"
-val acgT = Sign.read_typ (the_context (), K NONE) "acg"
+val scgT = @{typ scg}
+val acgT = @{typ acg}
fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
@@ -29,12 +29,12 @@
val stepP_const = "SCT_Interpretation.stepP"
val stepP_def = thm "SCT_Interpretation.stepP.simps"
-fun mk_stepP RD1 RD2 M1 M2 Rel =
+fun mk_stepP RD1 RD2 M1 M2 Rel =
let val RDT = fastype_of RD1
val MT = fastype_of M1
- in
- Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT)
- $ RD1 $ RD2 $ M1 $ M2 $ Rel
+ in
+ Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT)
+ $ RD1 $ RD2 $ M1 $ M2 $ Rel
end
val no_stepI = thm "SCT_Interpretation.no_stepI"
@@ -44,7 +44,7 @@
val approx_less = thm "SCT_Interpretation.approx_less"
val approx_leq = thm "SCT_Interpretation.approx_leq"
-fun mk_approx G RD1 RD2 Ms1 Ms2 =
+fun mk_approx G RD1 RD2 Ms1 Ms2 =
let val RDT = fastype_of RD1
val MsT = fastype_of Ms1
in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end
@@ -74,7 +74,7 @@
(* --> Library? *)
fun del_index n [] = []
| del_index n (x :: xs) =
- if n>0 then x :: del_index (n - 1) xs else xs
+ if n>0 then x :: del_index (n - 1) xs else xs
(* Lists as finite multisets *)
@@ -91,8 +91,8 @@
(Free (n, T), body)
end
| dest_ex _ = raise Match
-
-fun dest_all_ex (t as (Const ("Ex",_) $ _)) =
+
+fun dest_all_ex (t as (Const ("Ex",_) $ _)) =
let
val (v,b) = dest_ex t
val (vs, b') = dest_all_ex b
@@ -102,7 +102,7 @@
| dest_all_ex t = ([],t)
fun dist_vars [] vs = (null vs orelse error "dist_vars"; [])
- | dist_vars (T::Ts) vs =
+ | dist_vars (T::Ts) vs =
case find_index (fn v => fastype_of v = T) vs of
~1 => Free ("", T) :: dist_vars Ts vs
| i => (nth vs i) :: dist_vars Ts (del_index i vs)
@@ -111,7 +111,7 @@
let
val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
- in
+ in
foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
end
@@ -119,7 +119,7 @@
| bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
(* Builds relation descriptions from a relation definition *)
-fun mk_reldescs (Abs a) =
+fun mk_reldescs (Abs a) =
let
val (_, Abs a') = Term.dest_abs a
val (_, b) = Term.dest_abs a'
@@ -127,7 +127,7 @@
val (vss, bs) = split_list (map dest_all_ex cases)
val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) []
val rebind = map (bind_many o dist_vars unionTs) vss
-
+
val RDs = map2 dest_case rebind bs
in
HOLogic.mk_list (fastype_of (hd RDs)) RDs
@@ -177,7 +177,7 @@
val get_elem = snd o Logic.dest_equals o prop_of
-fun inst_nums thy i j (t:thm) =
+fun inst_nums thy i j (t:thm) =
instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t
datatype call_fact =
@@ -204,8 +204,8 @@
|> cterm_of thy
|> Goal.init
|> CLASIMPSET auto_tac |> Seq.hd
-
- val no_step = saved_state
+
+ val no_step = saved_state
|> forall_intr (cterm_of thy relvar)
|> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
|> CLASIMPSET auto_tac |> Seq.hd
@@ -216,15 +216,15 @@
else
let
fun set_m1 i =
- let
+ let
val M1 = nth Mst1 i
val with_m1 = saved_state
|> forall_intr (cterm_of thy mvar1)
|> forall_elim (cterm_of thy M1)
|> CLASIMPSET auto_tac |> Seq.hd
- fun set_m2 j =
- let
+ fun set_m2 j =
+ let
val M2 = nth Mst2 j
val with_m2 = with_m1
|> forall_intr (cterm_of thy mvar2)
@@ -241,10 +241,10 @@
val thm1 = decr with_m2
in
- if Thm.no_prems thm1
+ if Thm.no_prems thm1
then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
else let val thm2 = decreq with_m2 in
- if Thm.no_prems thm2
+ if Thm.no_prems thm2
then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
else all_tac end
end
@@ -255,7 +255,7 @@
val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
THEN (rtac approx_empty 1)
- val approx_thm = goal
+ val approx_thm = goal
|> cterm_of thy
|> Goal.init
|> tac |> Seq.hd
@@ -279,22 +279,22 @@
val pr_graph = Sign.string_of_term
fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X")
-val in_graph_tac =
+val in_graph_tac =
simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
| approx_tac (Graph (G, thm)) =
- rtac disjI2 1
+ rtac disjI2 1
THEN rtac exI 1
THEN rtac conjI 1
THEN rtac thm 2
THEN in_graph_tac
fun all_less_tac [] = rtac all_less_zero 1
- | all_less_tac (t :: ts) = rtac all_less_Suc 1
+ | all_less_tac (t :: ts) = rtac all_less_Suc 1
THEN simp_nth_tac 1
- THEN t
+ THEN t
THEN all_less_tac ts
@@ -310,7 +310,7 @@
val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
val RDs = HOLogic.dest_list RDlist
- val n = length RDs
+ val n = length RDs
val Mss = map measures_of RDs
@@ -329,7 +329,7 @@
val indices = (n - 1 downto 0)
val pairs = matrix indices indices
val parts = map_matrix (fn (n,m) =>
- (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
+ (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
(setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
@@ -337,7 +337,7 @@
pr_graph thy G ^ ",\n")
| _ => I) cs) parts ""
val _ = Output.warning s
-
+
val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
|> mk_set (edgeT HOLogic.natT scgT)
@@ -346,18 +346,19 @@
val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
- val tac =
+ val tac =
(SIMPSET (unfold_tac [sound_int_def, len_simp]))
THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
in
tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
end
-
+
-end
+end
+
--- a/src/HOL/Modelcheck/mucke_oracle.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Sat Apr 14 17:35:52 2007 +0200
@@ -218,7 +218,7 @@
fun deliver_erg sg tl _ [] = [] |
deliver_erg sg tl typ ((c,tyl)::r) = let
val ft = fun_type_of (rev tyl) typ;
- val trm = #t(rep_cterm(read_cterm sg (c,ft)));
+ val trm = Sign.simple_read_term sg ft c;
in
(con_term_list_of trm (arglist_of sg tl tyl))
@(deliver_erg sg tl typ r)
@@ -658,7 +658,7 @@
val arglist = arglist_of sg tl (snd c);
val tty = type_of_term t;
val con_typ = fun_type_of (rev (snd c)) tty;
- val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
+ val con = Sign.simple_read_term sg con_typ (fst c);
in
replace_termlist_with_args sg tl a con arglist t (l1,l2)
end |
@@ -746,7 +746,7 @@
let
val arglist = arglist_of sg tl (snd c);
val con_typ = fun_type_of (rev (snd c)) ty;
- val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
+ val con = Sign.simple_read_term sg con_typ (fst c);
fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
casc_if2 sg tl x con (a::r) ty trm cl =
--- a/src/HOL/Nominal/nominal_package.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Sat Apr 14 17:35:52 2007 +0200
@@ -123,7 +123,7 @@
fun read_typ sign ((Ts, sorts), str) =
let
- val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
+ val T = Type.no_tvars (Sign.read_def_typ (sign, (AList.lookup op =)
(map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
--- a/src/HOL/Tools/datatype_package.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Sat Apr 14 17:35:52 2007 +0200
@@ -157,7 +157,7 @@
val (types, sorts) = types_sorts state;
fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
| types' ixn = types ixn;
- val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
+ val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, TypeInfer.logicT)];
in case #T (rep_cterm ct) of
Type (tn, _) => tn
| _ => error ("Cannot determine type of " ^ quote aterm)
@@ -519,7 +519,7 @@
fun read_typ sign ((Ts, sorts), str) =
let
- val T = Type.no_tvars (Sign.read_typ (sign, AList.lookup (op =)
+ val T = Type.no_tvars (Sign.read_def_typ (sign, AList.lookup (op =)
(map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
--- a/src/HOL/Tools/inductive_package.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sat Apr 14 17:35:52 2007 +0200
@@ -74,7 +74,7 @@
val notTrueE = TrueI RSN (2, notE);
val notFalseI = Seq.hd (atac 1 notI);
val simp_thms' = map (fn s => mk_meta_eq (the (find_first
- (equal (term_of (read_cterm HOL.thy (s, propT))) o prop_of) simp_thms)))
+ (equal (Sign.read_prop HOL.thy s) o prop_of) simp_thms)))
["(~True) = False", "(~False) = True",
"(True --> ?P) = ?P", "(False --> ?P) = True",
"(?P & True) = ?P", "(True & ?P) = ?P"];
--- a/src/HOL/Tools/record_package.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Sat Apr 14 17:35:52 2007 +0200
@@ -1348,7 +1348,7 @@
(* prepare arguments *)
fun read_raw_parent sign s =
- (case Sign.read_typ_abbrev (sign, K NONE) s handle TYPE (msg, _, _) => error msg of
+ (case Sign.read_typ_abbrev sign s handle TYPE (msg, _, _) => error msg of
Type (name, Ts) => (Ts, name)
| _ => error ("Bad parent record specification: " ^ quote s));
@@ -1356,7 +1356,8 @@
let
fun def_sort (x, ~1) = AList.lookup (op =) env x
| def_sort _ = NONE;
- val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
+ val T = Type.no_tvars (Sign.read_def_typ (sign, def_sort) s)
+ handle TYPE (msg, _, _) => error msg;
in (Term.add_typ_tfrees (T, env), T) end;
fun cert_typ sign (env, raw_T) =
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Apr 14 17:35:52 2007 +0200
@@ -132,7 +132,7 @@
(* making a constructor set from a constructor term (of signature) *)
fun constr_set_string thy atyp ctstr =
let
-val trm = #t(rep_cterm(read_cterm thy (ctstr,atyp)));
+val trm = Sign.simple_read_term thy atyp ctstr;
val l = free_vars_of trm
in
if (check_for_constr thy atyp trm) then
@@ -149,7 +149,7 @@
fun hd_of (Const(a,_)) = a |
hd_of (t $ _) = hd_of t |
hd_of _ = raise malformed;
-val trm = #t(rep_cterm(read_cterm thy (s,#T(rep_ctyp(read_ctyp thy atypstr))) ))
+val trm = Sign.simple_read_term thy (Sign.read_typ thy atypstr) s;
in
hd_of trm handle malformed =>
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
@@ -177,8 +177,8 @@
(where bool indicates whether there is a precondition *)
fun extend thy atyp statetupel (actstr,r,[]) =
let
-val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
-val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
+val trm = Sign.simple_read_term thy atyp actstr;
+val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm)
@@ -191,8 +191,8 @@
fun pseudo_poststring [] = "" |
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
-val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
-val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
+val trm = Sign.simple_read_term thy atyp actstr;
+val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm) then
@@ -330,10 +330,10 @@
(writeln("Constructing automaton " ^ automaton_name ^ " ...");
let
val state_type_string = type_product_of_varlist(statetupel);
-val styp = #T(rep_ctyp (read_ctyp thy state_type_string)) ;
+val styp = Sign.read_typ thy state_type_string;
val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
-val atyp = #T(rep_ctyp (read_ctyp thy action_type));
+val atyp = Sign.read_typ thy action_type;
val inp_set_string = action_set_string thy atyp inp;
val out_set_string = action_set_string thy atyp out;
val int_set_string = action_set_string thy atyp int;
@@ -364,8 +364,8 @@
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
"_initial, " ^ automaton_name ^ "_trans,{},{})")
])
-val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm thy2
-( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[]))))));
+val chk_prime_list = (check_free_primed (Sign.simple_read_term thy2 (Type("bool",[]))
+( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
in
(
if (chk_prime_list = []) then thy2
--- a/src/HOLCF/cont_consts.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOLCF/cont_consts.ML Sat Apr 14 17:35:52 2007 +0200
@@ -80,7 +80,7 @@
fun gen_add_consts prep_typ raw_decls thy =
let
- val decls = map (upd_second (Thm.typ_of o prep_typ thy)) raw_decls;
+ val decls = map (upd_second (prep_typ thy)) raw_decls;
val (contconst_decls, normal_decls) = List.partition is_contconst decls;
val transformed_decls = map transform contconst_decls;
in
@@ -91,8 +91,8 @@
|> Theory.add_trrules_i (List.concat (map third transformed_decls))
end;
-val add_consts = gen_add_consts Thm.read_ctyp;
-val add_consts_i = gen_add_consts Thm.ctyp_of;
+val add_consts = gen_add_consts Sign.read_typ;
+val add_consts_i = gen_add_consts Sign.certify_typ;
(* outer syntax *)
--- a/src/HOLCF/domain/extender.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOLCF/domain/extender.ML Sat Apr 14 17:35:52 2007 +0200
@@ -100,7 +100,7 @@
fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
let
val dtnvs = map ((fn (dname,vs) =>
- (Sign.full_name thy''' dname, map (str2typ thy''') vs))
+ (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
@@ -139,7 +139,7 @@
end;
val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain str2typ;
+val add_domain = gen_add_domain Sign.read_typ;
(** outer syntax **)
--- a/src/HOLCF/domain/library.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOLCF/domain/library.ML Sat Apr 14 17:35:52 2007 +0200
@@ -75,7 +75,6 @@
fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
-fun str2typ sg = typ_of o read_ctyp sg;
(* ----- constructor list handling ----- *)
--- a/src/Provers/splitter.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/Provers/splitter.ML Sat Apr 14 17:35:52 2007 +0200
@@ -103,7 +103,7 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *)
val lift =
- let val ct = read_cterm Pure.thy
+ let val ct = Thm.read_cterm Pure.thy
("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
\P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
in OldGoals.prove_goalw_cterm [] ct
--- a/src/Pure/Proof/extraction.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Sat Apr 14 17:35:52 2007 +0200
@@ -218,7 +218,7 @@
fun read_condeq thy =
let val thy' = add_syntax thy
in fn s =>
- let val t = Logic.varify (term_of (read_cterm thy' (s, propT)))
+ let val t = Logic.varify (Sign.read_prop thy' s)
in (map Logic.dest_equals (Logic.strip_imp_prems t),
Logic.dest_equals (Logic.strip_imp_concl t))
end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
@@ -324,7 +324,7 @@
val T = etype_of thy' vs [] prop;
val (T', thw) = Type.freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
- val t = map_types thw (term_of (read_cterm thy' (s1, T')));
+ val t = map_types thw (Sign.simple_read_term thy' T' s1);
val r' = freeze_thaw (condrew thy' eqns
(procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
--- a/src/Pure/Proof/proof_syntax.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sat Apr 14 17:35:52 2007 +0200
@@ -236,9 +236,7 @@
|> add_proof_syntax
|> add_proof_atom_consts
(map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
- in
- fn T => fn s => Thm.term_of (read_cterm thy' (s, T))
- end;
+ in Sign.simple_read_term thy' end;
fun read_proof thy =
let val rd = read_term thy proofT
--- a/src/Pure/old_goals.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/Pure/old_goals.ML Sat Apr 14 17:35:52 2007 +0200
@@ -111,7 +111,7 @@
fun init_mkresult _ = error "No goal has been supplied in subgoal module";
val curr_mkresult = ref (init_mkresult: bool*thm->thm);
-val dummy = Thm.trivial (read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
+val dummy = Thm.trivial (Thm.read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
(*List of previous goal stacks, for the undo operation. Set by setstate.
A list of lists!*)
@@ -245,7 +245,7 @@
(*Version taking the goal as a string*)
fun prove_goalw thy rths agoal tacsf =
- let val chorn = read_cterm thy (agoal, propT)
+ let val chorn = Thm.read_cterm thy (agoal, propT)
in prove_goalw_cterm_general true rths chorn tacsf end
handle ERROR msg => cat_error msg (*from read_cterm?*)
("The error(s) above occurred for " ^ quote agoal);
@@ -359,7 +359,7 @@
(*Version taking the goal as a string*)
fun agoalw atomic thy rths agoal =
- agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
+ agoalw_cterm atomic rths (Thm.read_cterm thy (agoal, propT))
handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
("The error(s) above occurred for " ^ quote agoal);
--- a/src/ZF/Tools/inductive_package.ML Sat Apr 14 11:05:12 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Apr 14 17:35:52 2007 +0200
@@ -274,7 +274,7 @@
(Thm.assume A RS elim)
|> Drule.standard';
fun mk_cases a = make_cases (*delayed evaluation of body!*)
- (simpset ()) (read_cterm (Thm.theory_of_thm elim) (a, propT));
+ (simpset ()) (Thm.read_cterm (Thm.theory_of_thm elim) (a, propT));
fun induction_rules raw_induct thy =
let