cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
authorwenzelm
Sat Apr 14 17:35:52 2007 +0200 (2007-04-14)
changeset 22675acf10be7dcca
parent 22674 1a610904bbca
child 22676 522f4f8aa297
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
src/FOLP/simp.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Library/sct.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/cont_consts.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/library.ML
src/Provers/splitter.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/old_goals.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOLP/simp.ML	Sat Apr 14 11:05:12 2007 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat Apr 14 17:35:52 2007 +0200
     1.3 @@ -591,13 +591,14 @@
     1.4  fun mk_congs thy = List.concat o map (mk_cong_thy thy);
     1.5  
     1.6  fun mk_typed_congs thy =
     1.7 -let val S0 = Sign.defaultS thy;
     1.8 -    fun readfT(f,s) =
     1.9 -        let val T = Logic.incr_tvar 9 (Sign.read_typ(thy, K(SOME(S0))) s);
    1.10 -            val t = case Sign.const_type thy f of
    1.11 -                      SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.12 -        in (t,T) end
    1.13 +let
    1.14 +  fun readfT(f,s) =
    1.15 +    let
    1.16 +      val T = Logic.incr_tvar 9 (Sign.read_typ thy s);
    1.17 +      val t = case Sign.const_type thy f of
    1.18 +                  SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.19 +    in (t,T) end
    1.20  in List.concat o map (mk_cong_type thy o readfT) end;
    1.21  
    1.22 -end (* local *)
    1.23 -end (* SIMP *);
    1.24 +end;
    1.25 +end;
     2.1 --- a/src/HOL/Import/import_syntax.ML	Sat Apr 14 11:05:12 2007 +0200
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Sat Apr 14 17:35:52 2007 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4  					 val thyname = get_import_thy thy
     2.5  				     in
     2.6  					 Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
     2.7 -						 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp thy ty)) thy) (thy,constmaps)
     2.8 +						 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Sign.read_typ thy ty) thy) (thy,constmaps)
     2.9  				     end)
    2.10  
    2.11  val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
    2.12 @@ -147,7 +147,7 @@
    2.13  					  val thyname = get_import_thy thy
    2.14  				      in
    2.15  					  Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
    2.16 -						  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp thy ty)) thy) (thy,constmaps)
    2.17 +						  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Sign.read_typ thy ty) thy) (thy,constmaps)
    2.18  				      end)
    2.19  
    2.20  fun import_thy s =
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Apr 14 11:05:12 2007 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Apr 14 17:35:52 2007 +0200
     3.3 @@ -225,7 +225,7 @@
     3.4  	fun F n =
     3.5  	    let
     3.6  		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
     3.7 -		val cu  = read_cterm thy (str,T)
     3.8 +		val cu  = Thm.read_cterm thy (str,T)
     3.9  	    in
    3.10  		if match cu
    3.11  		then quote str
    3.12 @@ -473,10 +473,10 @@
    3.13  val check_name_thy = theory "Main"
    3.14  
    3.15  fun valid_boundvarname s =
    3.16 -  can (fn () => read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
    3.17 +  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", TypeInfer.logicT)) ();
    3.18  
    3.19  fun valid_varname s =
    3.20 -  can (fn () => read_cterm check_name_thy (s, TypeInfer.logicT)) ();
    3.21 +  can (fn () => Thm.read_cterm check_name_thy (s, TypeInfer.logicT)) ();
    3.22  
    3.23  fun protect_varname s =
    3.24      if innocent_varname s andalso valid_varname s then s else
     4.1 --- a/src/HOL/Library/sct.ML	Sat Apr 14 11:05:12 2007 +0200
     4.2 +++ b/src/HOL/Library/sct.ML	Sat Apr 14 17:35:52 2007 +0200
     4.3 @@ -4,13 +4,13 @@
     4.4  
     4.5  Tactics for size change termination.
     4.6  *)
     4.7 -signature SCT = 
     4.8 +signature SCT =
     4.9  sig
    4.10    val abs_rel_tac : tactic
    4.11    val mk_call_graph : tactic
    4.12  end
    4.13  
    4.14 -structure Sct : SCT = 
    4.15 +structure Sct : SCT =
    4.16  struct
    4.17  
    4.18  fun matrix [] ys = []
    4.19 @@ -18,8 +18,8 @@
    4.20  
    4.21  fun map_matrix f xss = map (map f) xss
    4.22  
    4.23 -val scgT = Sign.read_typ (the_context (), K NONE) "scg"
    4.24 -val acgT = Sign.read_typ (the_context (), K NONE) "acg"
    4.25 +val scgT = @{typ scg}
    4.26 +val acgT = @{typ acg}
    4.27  
    4.28  fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
    4.29  fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
    4.30 @@ -29,12 +29,12 @@
    4.31  val stepP_const = "SCT_Interpretation.stepP"
    4.32  val stepP_def = thm "SCT_Interpretation.stepP.simps"
    4.33  
    4.34 -fun mk_stepP RD1 RD2 M1 M2 Rel = 
    4.35 +fun mk_stepP RD1 RD2 M1 M2 Rel =
    4.36      let val RDT = fastype_of RD1
    4.37        val MT = fastype_of M1
    4.38 -    in 
    4.39 -      Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT) 
    4.40 -            $ RD1 $ RD2 $ M1 $ M2 $ Rel 
    4.41 +    in
    4.42 +      Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT)
    4.43 +            $ RD1 $ RD2 $ M1 $ M2 $ Rel
    4.44      end
    4.45  
    4.46  val no_stepI = thm "SCT_Interpretation.no_stepI"
    4.47 @@ -44,7 +44,7 @@
    4.48  val approx_less = thm "SCT_Interpretation.approx_less"
    4.49  val approx_leq = thm "SCT_Interpretation.approx_leq"
    4.50  
    4.51 -fun mk_approx G RD1 RD2 Ms1 Ms2 = 
    4.52 +fun mk_approx G RD1 RD2 Ms1 Ms2 =
    4.53      let val RDT = fastype_of RD1
    4.54        val MsT = fastype_of Ms1
    4.55      in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end
    4.56 @@ -74,7 +74,7 @@
    4.57  (* --> Library? *)
    4.58  fun del_index n [] = []
    4.59    | del_index n (x :: xs) =
    4.60 -    if n>0 then x :: del_index (n - 1) xs else xs 
    4.61 +    if n>0 then x :: del_index (n - 1) xs else xs
    4.62  
    4.63  (* Lists as finite multisets *)
    4.64  
    4.65 @@ -91,8 +91,8 @@
    4.66        (Free (n, T), body)
    4.67      end
    4.68    | dest_ex _ = raise Match
    4.69 -                         
    4.70 -fun dest_all_ex (t as (Const ("Ex",_) $ _)) = 
    4.71 +
    4.72 +fun dest_all_ex (t as (Const ("Ex",_) $ _)) =
    4.73      let
    4.74        val (v,b) = dest_ex t
    4.75        val (vs, b') = dest_all_ex b
    4.76 @@ -102,7 +102,7 @@
    4.77    | dest_all_ex t = ([],t)
    4.78  
    4.79  fun dist_vars [] vs = (null vs orelse error "dist_vars"; [])
    4.80 -  | dist_vars (T::Ts) vs = 
    4.81 +  | dist_vars (T::Ts) vs =
    4.82      case find_index (fn v => fastype_of v = T) vs of
    4.83        ~1 => Free ("", T) :: dist_vars Ts vs
    4.84      |  i => (nth vs i) :: dist_vars Ts (del_index i vs)
    4.85 @@ -111,7 +111,7 @@
    4.86      let
    4.87        val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
    4.88        val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
    4.89 -    in 
    4.90 +    in
    4.91        foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
    4.92      end
    4.93  
    4.94 @@ -119,7 +119,7 @@
    4.95    | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
    4.96  
    4.97  (* Builds relation descriptions from a relation definition *)
    4.98 -fun mk_reldescs (Abs a) = 
    4.99 +fun mk_reldescs (Abs a) =
   4.100      let
   4.101        val (_, Abs a') = Term.dest_abs a
   4.102        val (_, b) = Term.dest_abs a'
   4.103 @@ -127,7 +127,7 @@
   4.104        val (vss, bs) = split_list (map dest_all_ex cases)
   4.105        val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) []
   4.106        val rebind = map (bind_many o dist_vars unionTs) vss
   4.107 -                 
   4.108 +
   4.109        val RDs = map2 dest_case rebind bs
   4.110      in
   4.111        HOLogic.mk_list (fastype_of (hd RDs)) RDs
   4.112 @@ -177,7 +177,7 @@
   4.113  
   4.114  val get_elem = snd o Logic.dest_equals o prop_of
   4.115  
   4.116 -fun inst_nums thy i j (t:thm) = 
   4.117 +fun inst_nums thy i j (t:thm) =
   4.118    instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t
   4.119  
   4.120  datatype call_fact =
   4.121 @@ -204,8 +204,8 @@
   4.122                           |> cterm_of thy
   4.123                           |> Goal.init
   4.124                           |> CLASIMPSET auto_tac |> Seq.hd
   4.125 -                         
   4.126 -      val no_step = saved_state 
   4.127 +
   4.128 +      val no_step = saved_state
   4.129                        |> forall_intr (cterm_of thy relvar)
   4.130                        |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
   4.131                        |> CLASIMPSET auto_tac |> Seq.hd
   4.132 @@ -216,15 +216,15 @@
   4.133        else
   4.134          let
   4.135            fun set_m1 i =
   4.136 -              let 
   4.137 +              let
   4.138                  val M1 = nth Mst1 i
   4.139                  val with_m1 = saved_state
   4.140                                  |> forall_intr (cterm_of thy mvar1)
   4.141                                  |> forall_elim (cterm_of thy M1)
   4.142                                  |> CLASIMPSET auto_tac |> Seq.hd
   4.143  
   4.144 -                fun set_m2 j = 
   4.145 -                    let 
   4.146 +                fun set_m2 j =
   4.147 +                    let
   4.148                        val M2 = nth Mst2 j
   4.149                        val with_m2 = with_m1
   4.150                                        |> forall_intr (cterm_of thy mvar2)
   4.151 @@ -241,10 +241,10 @@
   4.152  
   4.153                        val thm1 = decr with_m2
   4.154                      in
   4.155 -                      if Thm.no_prems thm1 
   4.156 +                      if Thm.no_prems thm1
   4.157                        then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
   4.158                        else let val thm2 = decreq with_m2 in
   4.159 -                             if Thm.no_prems thm2 
   4.160 +                             if Thm.no_prems thm2
   4.161                               then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
   4.162                               else all_tac end
   4.163                      end
   4.164 @@ -255,7 +255,7 @@
   4.165            val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
   4.166                        THEN (rtac approx_empty 1)
   4.167  
   4.168 -          val approx_thm = goal 
   4.169 +          val approx_thm = goal
   4.170                      |> cterm_of thy
   4.171                      |> Goal.init
   4.172                      |> tac |> Seq.hd
   4.173 @@ -279,22 +279,22 @@
   4.174  val pr_graph = Sign.string_of_term
   4.175  fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X")
   4.176  
   4.177 -val in_graph_tac = 
   4.178 +val in_graph_tac =
   4.179      simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
   4.180      THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
   4.181  
   4.182  fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
   4.183    | approx_tac (Graph (G, thm)) =
   4.184 -    rtac disjI2 1 
   4.185 +    rtac disjI2 1
   4.186      THEN rtac exI 1
   4.187      THEN rtac conjI 1
   4.188      THEN rtac thm 2
   4.189      THEN in_graph_tac
   4.190  
   4.191  fun all_less_tac [] = rtac all_less_zero 1
   4.192 -  | all_less_tac (t :: ts) = rtac all_less_Suc 1 
   4.193 +  | all_less_tac (t :: ts) = rtac all_less_Suc 1
   4.194                                    THEN simp_nth_tac 1
   4.195 -                                  THEN t 
   4.196 +                                  THEN t
   4.197                                    THEN all_less_tac ts
   4.198  
   4.199  
   4.200 @@ -310,7 +310,7 @@
   4.201        val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
   4.202  
   4.203        val RDs = HOLogic.dest_list RDlist
   4.204 -      val n = length RDs 
   4.205 +      val n = length RDs
   4.206  
   4.207        val Mss = map measures_of RDs
   4.208  
   4.209 @@ -329,7 +329,7 @@
   4.210        val indices = (n - 1 downto 0)
   4.211        val pairs = matrix indices indices
   4.212        val parts = map_matrix (fn (n,m) =>
   4.213 -                                 (timeap_msg (string_of_int n ^ "," ^ string_of_int m) 
   4.214 +                                 (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
   4.215                                               (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
   4.216  
   4.217  
   4.218 @@ -337,7 +337,7 @@
   4.219                                                                              pr_graph thy G ^ ",\n")
   4.220                                                       | _ => I) cs) parts ""
   4.221        val _ = Output.warning s
   4.222 -  
   4.223 +
   4.224  
   4.225        val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
   4.226                      |> mk_set (edgeT HOLogic.natT scgT)
   4.227 @@ -346,18 +346,19 @@
   4.228  
   4.229        val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
   4.230  
   4.231 -      val tac = 
   4.232 +      val tac =
   4.233            (SIMPSET (unfold_tac [sound_int_def, len_simp]))
   4.234              THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
   4.235      in
   4.236        tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
   4.237      end
   4.238 -                  
   4.239 +
   4.240  
   4.241 -end                   
   4.242 +end
   4.243  
   4.244  
   4.245  
   4.246  
   4.247  
   4.248  
   4.249 +
     5.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Sat Apr 14 11:05:12 2007 +0200
     5.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sat Apr 14 17:35:52 2007 +0200
     5.3 @@ -218,7 +218,7 @@
     5.4    fun deliver_erg sg tl _ [] = [] |
     5.5    deliver_erg sg tl typ ((c,tyl)::r) = let
     5.6                          val ft = fun_type_of (rev tyl) typ;
     5.7 -                        val trm = #t(rep_cterm(read_cterm sg (c,ft)));
     5.8 +                        val trm = Sign.simple_read_term sg ft c;
     5.9                          in
    5.10                          (con_term_list_of trm (arglist_of sg tl tyl))
    5.11  			@(deliver_erg sg tl typ r)
    5.12 @@ -658,7 +658,7 @@
    5.13   val arglist = arglist_of sg tl (snd c);
    5.14   val tty = type_of_term t;
    5.15   val con_typ = fun_type_of (rev (snd c)) tty;
    5.16 - val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
    5.17 + val con = Sign.simple_read_term sg con_typ (fst c);
    5.18  in
    5.19   replace_termlist_with_args sg tl a con arglist t (l1,l2)
    5.20  end |
    5.21 @@ -746,7 +746,7 @@
    5.22  let
    5.23   val arglist = arglist_of sg tl (snd c);
    5.24   val con_typ = fun_type_of (rev (snd c)) ty;
    5.25 - val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
    5.26 + val con = Sign.simple_read_term sg con_typ (fst c);
    5.27   fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
    5.28   casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
    5.29   casc_if2 sg tl x con (a::r) ty trm cl =
     6.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat Apr 14 11:05:12 2007 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Apr 14 17:35:52 2007 +0200
     6.3 @@ -123,7 +123,7 @@
     6.4  
     6.5  fun read_typ sign ((Ts, sorts), str) =
     6.6    let
     6.7 -    val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
     6.8 +    val T = Type.no_tvars (Sign.read_def_typ (sign, (AList.lookup op =)
     6.9        (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
    6.10    in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
    6.11  
     7.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Apr 14 11:05:12 2007 +0200
     7.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Apr 14 17:35:52 2007 +0200
     7.3 @@ -157,7 +157,7 @@
     7.4      val (types, sorts) = types_sorts state;
     7.5      fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
     7.6        | types' ixn = types ixn;
     7.7 -    val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
     7.8 +    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, TypeInfer.logicT)];
     7.9    in case #T (rep_cterm ct) of
    7.10         Type (tn, _) => tn
    7.11       | _ => error ("Cannot determine type of " ^ quote aterm)
    7.12 @@ -519,7 +519,7 @@
    7.13  
    7.14  fun read_typ sign ((Ts, sorts), str) =
    7.15    let
    7.16 -    val T = Type.no_tvars (Sign.read_typ (sign, AList.lookup (op =)
    7.17 +    val T = Type.no_tvars (Sign.read_def_typ (sign, AList.lookup (op =)
    7.18        (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
    7.19    in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
    7.20  
     8.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Apr 14 11:05:12 2007 +0200
     8.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Apr 14 17:35:52 2007 +0200
     8.3 @@ -74,7 +74,7 @@
     8.4  val notTrueE = TrueI RSN (2, notE);
     8.5  val notFalseI = Seq.hd (atac 1 notI);
     8.6  val simp_thms' = map (fn s => mk_meta_eq (the (find_first
     8.7 -  (equal (term_of (read_cterm HOL.thy (s, propT))) o prop_of) simp_thms)))
     8.8 +  (equal (Sign.read_prop HOL.thy s) o prop_of) simp_thms)))
     8.9    ["(~True) = False", "(~False) = True",
    8.10     "(True --> ?P) = ?P", "(False --> ?P) = True",
    8.11     "(?P & True) = ?P", "(True & ?P) = ?P"];
     9.1 --- a/src/HOL/Tools/record_package.ML	Sat Apr 14 11:05:12 2007 +0200
     9.2 +++ b/src/HOL/Tools/record_package.ML	Sat Apr 14 17:35:52 2007 +0200
     9.3 @@ -1348,7 +1348,7 @@
     9.4  (* prepare arguments *)
     9.5  
     9.6  fun read_raw_parent sign s =
     9.7 -  (case Sign.read_typ_abbrev (sign, K NONE) s handle TYPE (msg, _, _) => error msg of
     9.8 +  (case Sign.read_typ_abbrev sign s handle TYPE (msg, _, _) => error msg of
     9.9      Type (name, Ts) => (Ts, name)
    9.10    | _ => error ("Bad parent record specification: " ^ quote s));
    9.11  
    9.12 @@ -1356,7 +1356,8 @@
    9.13    let
    9.14      fun def_sort (x, ~1) = AList.lookup (op =) env x
    9.15        | def_sort _ = NONE;
    9.16 -    val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
    9.17 +    val T = Type.no_tvars (Sign.read_def_typ (sign, def_sort) s)
    9.18 +      handle TYPE (msg, _, _) => error msg;
    9.19    in (Term.add_typ_tfrees (T, env), T) end;
    9.20  
    9.21  fun cert_typ sign (env, raw_T) =
    10.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Apr 14 11:05:12 2007 +0200
    10.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Apr 14 17:35:52 2007 +0200
    10.3 @@ -132,7 +132,7 @@
    10.4  (* making a constructor set from a constructor term (of signature) *)
    10.5  fun constr_set_string thy atyp ctstr =
    10.6  let
    10.7 -val trm = #t(rep_cterm(read_cterm thy (ctstr,atyp)));
    10.8 +val trm = Sign.simple_read_term thy atyp ctstr;
    10.9  val l = free_vars_of trm
   10.10  in
   10.11  if (check_for_constr thy atyp trm) then
   10.12 @@ -149,7 +149,7 @@
   10.13  fun hd_of (Const(a,_)) = a |
   10.14  hd_of (t $ _) = hd_of t |
   10.15  hd_of _ = raise malformed;
   10.16 -val trm = #t(rep_cterm(read_cterm thy (s,#T(rep_ctyp(read_ctyp thy atypstr))) ))
   10.17 +val trm = Sign.simple_read_term thy (Sign.read_typ thy atypstr) s;
   10.18  in
   10.19  hd_of trm handle malformed =>
   10.20  error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   10.21 @@ -177,8 +177,8 @@
   10.22  (where bool indicates whether there is a precondition *)
   10.23  fun extend thy atyp statetupel (actstr,r,[]) =
   10.24  let
   10.25 -val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
   10.26 -val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
   10.27 +val trm = Sign.simple_read_term thy atyp actstr;
   10.28 +val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
   10.29  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   10.30  in
   10.31  if (check_for_constr thy atyp trm)
   10.32 @@ -191,8 +191,8 @@
   10.33  fun pseudo_poststring [] = "" |
   10.34  pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
   10.35  pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
   10.36 -val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
   10.37 -val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
   10.38 +val trm = Sign.simple_read_term thy atyp actstr;
   10.39 +val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
   10.40  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   10.41  in
   10.42  if (check_for_constr thy atyp trm) then
   10.43 @@ -330,10 +330,10 @@
   10.44  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   10.45  let
   10.46  val state_type_string = type_product_of_varlist(statetupel);
   10.47 -val styp = #T(rep_ctyp (read_ctyp thy state_type_string)) ;
   10.48 +val styp = Sign.read_typ thy state_type_string;
   10.49  val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   10.50  val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   10.51 -val atyp = #T(rep_ctyp (read_ctyp thy action_type));
   10.52 +val atyp = Sign.read_typ thy action_type;
   10.53  val inp_set_string = action_set_string thy atyp inp;
   10.54  val out_set_string = action_set_string thy atyp out;
   10.55  val int_set_string = action_set_string thy atyp int;
   10.56 @@ -364,8 +364,8 @@
   10.57  automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   10.58  "_initial, " ^ automaton_name ^ "_trans,{},{})")
   10.59  ])
   10.60 -val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm thy2
   10.61 -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[]))))));
   10.62 +val chk_prime_list = (check_free_primed (Sign.simple_read_term thy2 (Type("bool",[]))
   10.63 +( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   10.64  in
   10.65  (
   10.66  if (chk_prime_list = []) then thy2
    11.1 --- a/src/HOLCF/cont_consts.ML	Sat Apr 14 11:05:12 2007 +0200
    11.2 +++ b/src/HOLCF/cont_consts.ML	Sat Apr 14 17:35:52 2007 +0200
    11.3 @@ -80,7 +80,7 @@
    11.4  
    11.5  fun gen_add_consts prep_typ raw_decls thy =
    11.6    let
    11.7 -    val decls = map (upd_second (Thm.typ_of o prep_typ thy)) raw_decls;
    11.8 +    val decls = map (upd_second (prep_typ thy)) raw_decls;
    11.9      val (contconst_decls, normal_decls) = List.partition is_contconst decls;
   11.10      val transformed_decls = map transform contconst_decls;
   11.11    in
   11.12 @@ -91,8 +91,8 @@
   11.13      |> Theory.add_trrules_i (List.concat (map third transformed_decls))
   11.14    end;
   11.15  
   11.16 -val add_consts = gen_add_consts Thm.read_ctyp;
   11.17 -val add_consts_i = gen_add_consts Thm.ctyp_of;
   11.18 +val add_consts = gen_add_consts Sign.read_typ;
   11.19 +val add_consts_i = gen_add_consts Sign.certify_typ;
   11.20  
   11.21  
   11.22  (* outer syntax *)
    12.1 --- a/src/HOLCF/domain/extender.ML	Sat Apr 14 11:05:12 2007 +0200
    12.2 +++ b/src/HOLCF/domain/extender.ML	Sat Apr 14 17:35:52 2007 +0200
    12.3 @@ -100,7 +100,7 @@
    12.4  fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
    12.5    let
    12.6      val dtnvs = map ((fn (dname,vs) => 
    12.7 -			 (Sign.full_name thy''' dname, map (str2typ thy''') vs))
    12.8 +			 (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
    12.9                     o fst) eqs''';
   12.10      val cons''' = map snd eqs''';
   12.11      fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
   12.12 @@ -139,7 +139,7 @@
   12.13    end;
   12.14  
   12.15  val add_domain_i = gen_add_domain Sign.certify_typ;
   12.16 -val add_domain = gen_add_domain str2typ;
   12.17 +val add_domain = gen_add_domain Sign.read_typ;
   12.18  
   12.19  
   12.20  (** outer syntax **)
    13.1 --- a/src/HOLCF/domain/library.ML	Sat Apr 14 11:05:12 2007 +0200
    13.2 +++ b/src/HOLCF/domain/library.ML	Sat Apr 14 17:35:52 2007 +0200
    13.3 @@ -75,7 +75,6 @@
    13.4  
    13.5  fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
    13.6  fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
    13.7 -fun str2typ sg = typ_of o read_ctyp sg;
    13.8  
    13.9  (* ----- constructor list handling ----- *)
   13.10  
    14.1 --- a/src/Provers/splitter.ML	Sat Apr 14 11:05:12 2007 +0200
    14.2 +++ b/src/Provers/splitter.ML	Sat Apr 14 17:35:52 2007 +0200
    14.3 @@ -103,7 +103,7 @@
    14.4  val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
    14.5  
    14.6  val lift =
    14.7 -  let val ct = read_cterm Pure.thy
    14.8 +  let val ct = Thm.read_cterm Pure.thy
    14.9             ("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
   14.10              \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
   14.11    in OldGoals.prove_goalw_cterm [] ct
    15.1 --- a/src/Pure/Proof/extraction.ML	Sat Apr 14 11:05:12 2007 +0200
    15.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 14 17:35:52 2007 +0200
    15.3 @@ -218,7 +218,7 @@
    15.4  fun read_condeq thy =
    15.5    let val thy' = add_syntax thy
    15.6    in fn s =>
    15.7 -    let val t = Logic.varify (term_of (read_cterm thy' (s, propT)))
    15.8 +    let val t = Logic.varify (Sign.read_prop thy' s)
    15.9      in (map Logic.dest_equals (Logic.strip_imp_prems t),
   15.10        Logic.dest_equals (Logic.strip_imp_concl t))
   15.11      end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
   15.12 @@ -324,7 +324,7 @@
   15.13        val T = etype_of thy' vs [] prop;
   15.14        val (T', thw) = Type.freeze_thaw_type
   15.15          (if T = nullT then nullT else map fastype_of vars' ---> T);
   15.16 -      val t = map_types thw (term_of (read_cterm thy' (s1, T')));
   15.17 +      val t = map_types thw (Sign.simple_read_term thy' T' s1);
   15.18        val r' = freeze_thaw (condrew thy' eqns
   15.19          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   15.20            (Const ("realizes", T --> propT --> propT) $
    16.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Apr 14 11:05:12 2007 +0200
    16.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Apr 14 17:35:52 2007 +0200
    16.3 @@ -236,9 +236,7 @@
    16.4        |> add_proof_syntax
    16.5        |> add_proof_atom_consts
    16.6          (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
    16.7 -  in
    16.8 -    fn T => fn s => Thm.term_of (read_cterm thy' (s, T))
    16.9 -  end;
   16.10 +  in Sign.simple_read_term thy' end;
   16.11  
   16.12  fun read_proof thy =
   16.13    let val rd = read_term thy proofT
    17.1 --- a/src/Pure/old_goals.ML	Sat Apr 14 11:05:12 2007 +0200
    17.2 +++ b/src/Pure/old_goals.ML	Sat Apr 14 17:35:52 2007 +0200
    17.3 @@ -111,7 +111,7 @@
    17.4  fun init_mkresult _ = error "No goal has been supplied in subgoal module";
    17.5  val curr_mkresult = ref (init_mkresult: bool*thm->thm);
    17.6  
    17.7 -val dummy = Thm.trivial (read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
    17.8 +val dummy = Thm.trivial (Thm.read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
    17.9  
   17.10  (*List of previous goal stacks, for the undo operation.  Set by setstate.
   17.11    A list of lists!*)
   17.12 @@ -245,7 +245,7 @@
   17.13  
   17.14  (*Version taking the goal as a string*)
   17.15  fun prove_goalw thy rths agoal tacsf =
   17.16 -  let val chorn = read_cterm thy (agoal, propT)
   17.17 +  let val chorn = Thm.read_cterm thy (agoal, propT)
   17.18    in prove_goalw_cterm_general true rths chorn tacsf end
   17.19    handle ERROR msg => cat_error msg (*from read_cterm?*)
   17.20                  ("The error(s) above occurred for " ^ quote agoal);
   17.21 @@ -359,7 +359,7 @@
   17.22  
   17.23  (*Version taking the goal as a string*)
   17.24  fun agoalw atomic thy rths agoal =
   17.25 -    agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
   17.26 +    agoalw_cterm atomic rths (Thm.read_cterm thy (agoal, propT))
   17.27      handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*)
   17.28          ("The error(s) above occurred for " ^ quote agoal);
   17.29  
    18.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Apr 14 11:05:12 2007 +0200
    18.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Apr 14 17:35:52 2007 +0200
    18.3 @@ -274,7 +274,7 @@
    18.4        (Thm.assume A RS elim)
    18.5        |> Drule.standard';
    18.6    fun mk_cases a = make_cases (*delayed evaluation of body!*)
    18.7 -    (simpset ()) (read_cterm (Thm.theory_of_thm elim) (a, propT));
    18.8 +    (simpset ()) (Thm.read_cterm (Thm.theory_of_thm elim) (a, propT));
    18.9  
   18.10    fun induction_rules raw_induct thy =
   18.11     let