# HG changeset patch # User wenzelm # Date 1176564952 -7200 # Node ID acf10be7dccadcdaf9146b88f998f988b28d4c8f # Parent 1a610904bbcad7861ae05ae6c959856e22ec7698 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; diff -r 1a610904bbca -r acf10be7dcca src/FOLP/simp.ML --- 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; diff -r 1a610904bbca -r acf10be7dcca src/HOL/Import/import_syntax.ML --- 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 = diff -r 1a610904bbca -r acf10be7dcca src/HOL/Import/proof_kernel.ML --- 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 diff -r 1a610904bbca -r acf10be7dcca src/HOL/Library/sct.ML --- 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 + diff -r 1a610904bbca -r acf10be7dcca src/HOL/Modelcheck/mucke_oracle.ML --- 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 = diff -r 1a610904bbca -r acf10be7dcca src/HOL/Nominal/nominal_package.ML --- 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; diff -r 1a610904bbca -r acf10be7dcca src/HOL/Tools/datatype_package.ML --- 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; diff -r 1a610904bbca -r acf10be7dcca src/HOL/Tools/inductive_package.ML --- 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"]; diff -r 1a610904bbca -r acf10be7dcca src/HOL/Tools/record_package.ML --- 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) = diff -r 1a610904bbca -r acf10be7dcca src/HOLCF/IOA/meta_theory/ioa_package.ML --- 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 diff -r 1a610904bbca -r acf10be7dcca src/HOLCF/cont_consts.ML --- 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 *) diff -r 1a610904bbca -r acf10be7dcca src/HOLCF/domain/extender.ML --- 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 **) diff -r 1a610904bbca -r acf10be7dcca src/HOLCF/domain/library.ML --- 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 ----- *) diff -r 1a610904bbca -r acf10be7dcca src/Provers/splitter.ML --- 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 diff -r 1a610904bbca -r acf10be7dcca src/Pure/Proof/extraction.ML --- 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) $ diff -r 1a610904bbca -r acf10be7dcca src/Pure/Proof/proof_syntax.ML --- 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 diff -r 1a610904bbca -r acf10be7dcca src/Pure/old_goals.ML --- 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); diff -r 1a610904bbca -r acf10be7dcca src/ZF/Tools/inductive_package.ML --- 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