Syntax.parse/check/read;
authorwenzelm
Tue Sep 25 13:28:37 2007 +0200 (2007-09-25)
changeset 24707dfeb98f84e93
parent 24706 c58547ff329b
child 24708 d9b00117365e
Syntax.parse/check/read;
src/FOLP/simp.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/specification_package.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/Tools/cont_consts.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/fixrec_package.ML
src/Provers/splitter.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code_unit.ML
src/Pure/Proof/extraction.ML
src/Pure/codegen.ML
src/Pure/meta_simplifier.ML
src/Pure/sign.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/FOLP/simp.ML	Tue Sep 25 13:28:35 2007 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Sep 25 13:28:37 2007 +0200
     1.3 @@ -594,7 +594,7 @@
     1.4  let
     1.5    fun readfT(f,s) =
     1.6      let
     1.7 -      val T = Logic.incr_tvar 9 (Sign.read_typ thy s);
     1.8 +      val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s);
     1.9        val t = case Sign.const_type thy f of
    1.10                    SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.11      in (t,T) end
     2.1 --- a/src/HOL/Import/import_syntax.ML	Tue Sep 25 13:28:35 2007 +0200
     2.2 +++ b/src/HOL/Import/import_syntax.ML	Tue Sep 25 13:28:37 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 (Sign.read_typ thy ty) thy) (thy,constmaps)
     2.8 +						 | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global 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 (Sign.read_typ thy ty) thy) (thy,constmaps)
    2.17 +						  | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global 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	Tue Sep 25 13:28:35 2007 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 25 13:28:37 2007 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4      type term
     3.5      type thm
     3.6      type ('a,'b) subst
     3.7 -	 
     3.8 +
     3.9      type proof_info
    3.10      datatype proof = Proof of proof_info * proof_content
    3.11  	 and proof_content
    3.12 @@ -111,8 +111,8 @@
    3.13      val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm
    3.14      val new_axiom : string -> term -> theory -> theory * thm
    3.15  
    3.16 -    val prin : term -> unit 
    3.17 -    val protect_factname : string -> string 
    3.18 +    val prin : term -> unit
    3.19 +    val protect_factname : string -> string
    3.20      val replay_protect_varname : string -> string -> unit
    3.21      val replay_add_dump : string -> theory -> theory
    3.22  end
    3.23 @@ -125,7 +125,7 @@
    3.24  type ('a,'b) subst = ('a * 'b) list
    3.25  datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
    3.26  
    3.27 -fun hthm2thm (HOLThm (_, th)) = th 
    3.28 +fun hthm2thm (HOLThm (_, th)) = th
    3.29  
    3.30  fun to_hol_thm th = HOLThm ([], th)
    3.31  
    3.32 @@ -134,7 +134,7 @@
    3.33  
    3.34  datatype proof_info
    3.35    = Info of {disk_info: (string * string) option ref}
    3.36 -	    
    3.37 +
    3.38  datatype proof = Proof of proof_info * proof_content
    3.39       and proof_content
    3.40         = PRefl of term
    3.41 @@ -176,7 +176,7 @@
    3.42  exception PK of string * string
    3.43  fun ERR f mesg = PK (f,mesg)
    3.44  
    3.45 -fun print_exn e = 
    3.46 +fun print_exn e =
    3.47      case e of
    3.48  	PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
    3.49        | _ => OldGoals.print_exn e
    3.50 @@ -213,21 +213,23 @@
    3.51  fun smart_string_of_cterm ct =
    3.52      let
    3.53  	val {thy,t,T,...} = rep_cterm ct
    3.54 +        val ctxt = ProofContext.init thy
    3.55          (* Hack to avoid parse errors with Trueprop *)
    3.56  	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    3.57  		   handle TERM _ => ct)
    3.58 -	fun match cu = t aconv (term_of cu)
    3.59 +	fun match u = t aconv u
    3.60  	fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
    3.61  	  | G 1 = Library.setmp show_brackets true (G 0)
    3.62  	  | G 2 = Library.setmp show_all_types true (G 0)
    3.63  	  | G 3 = Library.setmp show_brackets true (G 2)
    3.64 -          | G _ = raise SMART_STRING 
    3.65 +          | G _ = raise SMART_STRING
    3.66  	fun F n =
    3.67  	    let
    3.68  		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    3.69 -		val cu  = Thm.read_cterm thy (str,T)
    3.70 +		val u = Syntax.parse_term ctxt str
    3.71 +                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
    3.72  	    in
    3.73 -		if match cu
    3.74 +		if match u
    3.75  		then quote str
    3.76  		else F (n+1)
    3.77  	    end
    3.78 @@ -237,7 +239,7 @@
    3.79        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    3.80      end
    3.81      handle ERROR mesg => simple_smart_string_of_cterm ct
    3.82 - 
    3.83 +
    3.84  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    3.85  
    3.86  fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
    3.87 @@ -272,20 +274,20 @@
    3.88      in
    3.89  	F
    3.90      end
    3.91 -fun i mem L = 
    3.92 -    let fun itr [] = false 
    3.93 -	  | itr (a::rst) = i=a orelse itr rst 
    3.94 +fun i mem L =
    3.95 +    let fun itr [] = false
    3.96 +	  | itr (a::rst) = i=a orelse itr rst
    3.97      in itr L end;
    3.98 -    
    3.99 +
   3.100  fun insert i L = if i mem L then L else i::L
   3.101 -					
   3.102 +
   3.103  fun mk_set [] = []
   3.104    | mk_set (a::rst) = insert a (mk_set rst)
   3.105 -		      
   3.106 +
   3.107  fun [] union S = S
   3.108    | S union [] = S
   3.109    | (a::rst) union S2 = rst union (insert a S2)
   3.110 -			
   3.111 +
   3.112  fun implode_subst [] = []
   3.113    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
   3.114    | implode_subst _ = raise ERR "implode_subst" "malformed substitution list"
   3.115 @@ -300,7 +302,7 @@
   3.116  fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2))
   3.117  end
   3.118  
   3.119 -(* Acutal code. *)
   3.120 +(* Actual code. *)
   3.121  
   3.122  fun get_segment thyname l = (Lib.assoc "s" l
   3.123  			     handle PK _ => thyname)
   3.124 @@ -430,8 +432,8 @@
   3.125  
   3.126  fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
   3.127  
   3.128 -local 
   3.129 -  fun get_const sg thyname name = 
   3.130 +local
   3.131 +  fun get_const sg thyname name =
   3.132      (case Sign.const_type sg name of
   3.133        SOME ty => Const (name, ty)
   3.134      | NONE => raise ERR "get_type" (name ^ ": No such constant"))
   3.135 @@ -472,16 +474,16 @@
   3.136  val check_name_thy = theory "Main"
   3.137  
   3.138  fun valid_boundvarname s =
   3.139 -  can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) ();
   3.140 +  can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
   3.141  
   3.142  fun valid_varname s =
   3.143 -  can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) ();
   3.144 +  can (fn () => Syntax.read_term_global check_name_thy s) ();
   3.145  
   3.146  fun protect_varname s =
   3.147      if innocent_varname s andalso valid_varname s then s else
   3.148      case Symtab.lookup (!protected_varnames) s of
   3.149        SOME t => t
   3.150 -    | NONE => 
   3.151 +    | NONE =>
   3.152        let
   3.153  	  val _ = inc invented_isavar
   3.154  	  val t = "u_" ^ string_of_int (!invented_isavar)
   3.155 @@ -493,56 +495,56 @@
   3.156  
   3.157  exception REPLAY_PROTECT_VARNAME of string*string*string
   3.158  
   3.159 -fun replay_protect_varname s t = 
   3.160 +fun replay_protect_varname s t =
   3.161  	case Symtab.lookup (!protected_varnames) s of
   3.162  	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
   3.163 -	| NONE => 	
   3.164 +	| NONE =>
   3.165            let
   3.166  	      val _ = inc invented_isavar
   3.167  	      val t = "u_" ^ string_of_int (!invented_isavar)
   3.168                val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   3.169            in
   3.170  	      ()
   3.171 -          end	       	
   3.172 -	 
   3.173 +          end
   3.174 +
   3.175  fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
   3.176  
   3.177  fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   3.178    | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
   3.179    | mk_lambda v t = raise TERM ("lambda", [v, t]);
   3.180 - 
   3.181 -fun replacestr x y s = 
   3.182 +
   3.183 +fun replacestr x y s =
   3.184  let
   3.185    val xl = explode x
   3.186    val yl = explode y
   3.187    fun isprefix [] ys = true
   3.188      | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
   3.189 -    | isprefix _ _ = false  
   3.190 +    | isprefix _ _ = false
   3.191    fun isp s = isprefix xl s
   3.192    fun chg s = yl@(List.drop (s, List.length xl))
   3.193    fun r [] = []
   3.194 -    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) 
   3.195 +    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
   3.196  in
   3.197    implode(r (explode s))
   3.198 -end    
   3.199 +end
   3.200  
   3.201  fun protect_factname s = replacestr "." "_dot_" s
   3.202 -fun unprotect_factname s = replacestr "_dot_" "." s 
   3.203 +fun unprotect_factname s = replacestr "_dot_" "." s
   3.204  
   3.205  val ty_num_prefix = "N_"
   3.206  
   3.207  fun startsWithDigit s = Char.isDigit (hd (String.explode s))
   3.208  
   3.209 -fun protect_tyname tyn = 
   3.210 +fun protect_tyname tyn =
   3.211    let
   3.212 -    val tyn' = 
   3.213 -      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else 
   3.214 +    val tyn' =
   3.215 +      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
   3.216        (if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
   3.217    in
   3.218      tyn'
   3.219    end
   3.220  
   3.221 -fun protect_constname tcn = tcn 
   3.222 +fun protect_constname tcn = tcn
   3.223   (* if tcn = ".." then "dotdot"
   3.224    else if tcn = "==" then "eqeq"
   3.225    else tcn*)
   3.226 @@ -634,9 +636,9 @@
   3.227  	    in
   3.228  		mk_comb(f,a)
   3.229  	    end
   3.230 -	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 
   3.231 -	    let		
   3.232 -                val x = get_term_from_index thy thyname types terms tmx 
   3.233 +	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
   3.234 +	    let
   3.235 +                val x = get_term_from_index thy thyname types terms tmx
   3.236                  val a = get_term_from_index thy thyname types terms tma
   3.237  	    in
   3.238  		mk_lambda x a
   3.239 @@ -683,7 +685,7 @@
   3.240      in
   3.241  	Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
   3.242      end
   3.243 -			   
   3.244 +
   3.245  fun proof_file_name thyname thmname thy =
   3.246      let
   3.247  	val path = case get_proof_dir thyname thy of
   3.248 @@ -693,7 +695,7 @@
   3.249      in
   3.250  	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
   3.251      end
   3.252 -	
   3.253 +
   3.254  fun xml_to_proof thyname types terms prf thy =
   3.255      let
   3.256  	val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
   3.257 @@ -936,18 +938,18 @@
   3.258  	x2p prf
   3.259      end
   3.260  
   3.261 -fun import_proof_concl thyname thmname thy = 
   3.262 +fun import_proof_concl thyname thmname thy =
   3.263      let
   3.264  	val is = TextIO.openIn(proof_file_name thyname thmname thy)
   3.265  	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   3.266  	val _ = TextIO.closeIn is
   3.267 -    in 
   3.268 +    in
   3.269  	case proof_xml of
   3.270  	    Elem("proof",[],xtypes::xterms::prf::rest) =>
   3.271  	    let
   3.272  		val types = TypeNet.input_types thyname xtypes
   3.273  		val terms = TermNet.input_terms thyname types xterms
   3.274 -                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm               
   3.275 +                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
   3.276  	    in
   3.277  		case rest of
   3.278  		    [] => NONE
   3.279 @@ -962,7 +964,7 @@
   3.280  	val is = TextIO.openIn(proof_file_name thyname thmname thy)
   3.281  	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   3.282  	val _ = TextIO.closeIn is
   3.283 -    in 
   3.284 +    in
   3.285  	case proof_xml of
   3.286  	    Elem("proof",[],xtypes::xterms::prf::rest) =>
   3.287  	    let
   3.288 @@ -1068,7 +1070,7 @@
   3.289  	res
   3.290      end
   3.291  
   3.292 -val permute_prems = Thm.permute_prems 
   3.293 +val permute_prems = Thm.permute_prems
   3.294  
   3.295  fun rearrange sg tm th =
   3.296      let
   3.297 @@ -1152,26 +1154,26 @@
   3.298          | name_of _ = ERR "name_of"
   3.299        fun new_name' bump map n =
   3.300            let val n' = n^bump in
   3.301 -            if is_old_name n' orelse Symtab.lookup map n' <> NONE then 
   3.302 +            if is_old_name n' orelse Symtab.lookup map n' <> NONE then
   3.303                new_name' (Symbol.bump_string bump) map n
   3.304              else
   3.305                n'
   3.306 -          end              
   3.307 +          end
   3.308        val new_name = new_name' "a"
   3.309        fun replace_name n' (Free (n, t)) = Free (n', t)
   3.310          | replace_name n' _ = ERR "replace_name"
   3.311 -      (* map: old or fresh name -> old free, 
   3.312 +      (* map: old or fresh name -> old free,
   3.313           invmap: old free which has fresh name assigned to it -> fresh name *)
   3.314        fun dis (v, mapping as (map,invmap)) =
   3.315            let val n = name_of v in
   3.316              case Symtab.lookup map n of
   3.317                NONE => (Symtab.update (n, v) map, invmap)
   3.318 -            | SOME v' => 
   3.319 -              if v=v' then 
   3.320 -                mapping 
   3.321 +            | SOME v' =>
   3.322 +              if v=v' then
   3.323 +                mapping
   3.324                else
   3.325                  let val n' = new_name map n in
   3.326 -                  (Symtab.update (n', v) map, 
   3.327 +                  (Symtab.update (n', v) map,
   3.328                     Termtab.update (v, n') invmap)
   3.329                  end
   3.330            end
   3.331 @@ -1179,16 +1181,16 @@
   3.332        if (length freenames = length frees) then
   3.333          thm
   3.334        else
   3.335 -        let 
   3.336 -          val (_, invmap) = 
   3.337 -              List.foldl dis (Symtab.empty, Termtab.empty) frees 
   3.338 +        let
   3.339 +          val (_, invmap) =
   3.340 +              List.foldl dis (Symtab.empty, Termtab.empty) frees
   3.341            fun make_subst ((oldfree, newname), (intros, elims)) =
   3.342 -              (cterm_of thy oldfree :: intros, 
   3.343 +              (cterm_of thy oldfree :: intros,
   3.344                 cterm_of thy (replace_name newname oldfree) :: elims)
   3.345            val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
   3.346 -        in 
   3.347 +        in
   3.348            forall_elim_list elims (forall_intr_list intros thm)
   3.349 -        end     
   3.350 +        end
   3.351      end
   3.352  
   3.353  val debug = ref false
   3.354 @@ -1201,7 +1203,7 @@
   3.355  fun get_hol4_thm thyname thmname thy =
   3.356      case get_hol4_theorem thyname thmname thy of
   3.357  	SOME hth => SOME (HOLThm hth)
   3.358 -      | NONE => 
   3.359 +      | NONE =>
   3.360  	let
   3.361  	    val pending = HOL4Pending.get thy
   3.362  	in
   3.363 @@ -1215,7 +1217,7 @@
   3.364  			 c = "All" orelse
   3.365  			 c = "op -->" orelse
   3.366  			 c = "op &" orelse
   3.367 -			 c = "op =")) (Term.term_consts tm) 
   3.368 +			 c = "op =")) (Term.term_consts tm)
   3.369  
   3.370  fun match_consts t (* th *) =
   3.371      let
   3.372 @@ -1291,7 +1293,7 @@
   3.373  	    end
   3.374  	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
   3.375  	  | NONE =>
   3.376 -	    let		
   3.377 +	    let
   3.378  		val _ = (message "Looking for conclusion:";
   3.379  			 if_debug prin isaconc)
   3.380  		val cs = non_trivial_term_consts isaconc
   3.381 @@ -1325,7 +1327,7 @@
   3.382  	    val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
   3.383  	in
   3.384  	    case concl_of i2h_conc of
   3.385 -		Const("==",_) $ lhs $ _ => 
   3.386 +		Const("==",_) $ lhs $ _ =>
   3.387  		(warning ("Failed lookup of theorem '"^thmname^"':");
   3.388  	         writeln "Original conclusion:";
   3.389  		 prin hol4conc';
   3.390 @@ -1334,10 +1336,10 @@
   3.391  	      | _ => ()
   3.392  	end
   3.393    in
   3.394 -      case b of 
   3.395 +      case b of
   3.396  	  NONE => (warn () handle _ => (); (a,b))
   3.397  	| _ => (a, b)
   3.398 -  end 
   3.399 +  end
   3.400  
   3.401  fun get_thm thyname thmname thy =
   3.402      case get_hol4_thm thyname thmname thy of
   3.403 @@ -1373,11 +1375,11 @@
   3.404  	val rew = rewrite_hol4_term (concl_of th) thy
   3.405  	val th  = equal_elim rew th
   3.406  	val thy' = add_hol4_pending thyname thmname args thy
   3.407 -	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') 
   3.408 +	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   3.409          val th = disambiguate_frees th
   3.410  	val thy2 = if gen_output
   3.411 -		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ 
   3.412 -                                  (smart_string_of_thm th) ^ "\n  by (import " ^ 
   3.413 +		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
   3.414 +                                  (smart_string_of_thm th) ^ "\n  by (import " ^
   3.415                                    thyname ^ " " ^ (quotename thmname) ^ ")") thy'
   3.416  		   else thy'
   3.417      in
   3.418 @@ -1768,7 +1770,7 @@
   3.419      in
   3.420  	(thy,res)
   3.421      end
   3.422 -	
   3.423 +
   3.424  
   3.425  fun CCONTR tm hth thy =
   3.426      let
   3.427 @@ -1851,7 +1853,7 @@
   3.428  			      end) th vlist'
   3.429  		end
   3.430  	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
   3.431 -	      | NONE => 
   3.432 +	      | NONE =>
   3.433  		foldr (fn (v,th) => mk_ABS v th thy) th vlist'
   3.434  	val res = HOLThm(rens_of info',th1)
   3.435  	val _ = message "RESULT:"
   3.436 @@ -1947,7 +1949,7 @@
   3.437  			    val p3 = string_of_mixfix csyn
   3.438  			    val p4 = smart_string_of_cterm crhs
   3.439  			in
   3.440 -			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''  
   3.441 +			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
   3.442  			end
   3.443  		    else
   3.444  			(add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
   3.445 @@ -1958,7 +1960,7 @@
   3.446  		    | NONE => raise ERR "new_definition" "Bad conclusion"
   3.447  	val fullname = Sign.full_name thy22 thmname
   3.448  	val thy22' = case opt_get_output_thy thy22 of
   3.449 -			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; 
   3.450 +			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
   3.451  				add_hol4_mapping thyname thmname fullname thy22)
   3.452  		       | output_thy =>
   3.453  			 let
   3.454 @@ -1982,7 +1984,7 @@
   3.455  fun new_specification thyname thmname names hth thy =
   3.456      case HOL4DefThy.get thy of
   3.457  	Replaying _ => (thy,hth)
   3.458 -      | _ => 
   3.459 +      | _ =>
   3.460  	let
   3.461  	    val _ = message "NEW_SPEC:"
   3.462  	    val _ = if_debug pth hth
   3.463 @@ -2005,7 +2007,7 @@
   3.464  				   dest_eta_abs abody
   3.465  				 | dest_exists tm =
   3.466  				   raise ERR "new_specification" "Bad existential formula"
   3.467 -					 
   3.468 +
   3.469  			       val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
   3.470  							  let
   3.471  							      val (_,cT,p) = dest_exists ex
   3.472 @@ -2056,11 +2058,11 @@
   3.473  	    intern_store_thm false thyname thmname hth thy''
   3.474  	end
   3.475  	handle e => (message "exception in new_specification"; print_exn e)
   3.476 -		    
   3.477 +
   3.478  end
   3.479 -			   
   3.480 +
   3.481  fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
   3.482 -				      
   3.483 +
   3.484  fun to_isa_thm (hth as HOLThm(_,th)) =
   3.485      let
   3.486  	val (HOLThm args) = norm_hthm (theory_of_thm th) hth
   3.487 @@ -2079,7 +2081,7 @@
   3.488  fun new_type_definition thyname thmname tycname hth thy =
   3.489      case HOL4DefThy.get thy of
   3.490  	Replaying _ => (thy,hth)
   3.491 -      | _ => 
   3.492 +      | _ =>
   3.493  	let
   3.494  	    val _ = message "TYPE_DEF:"
   3.495  	    val _ = if_debug pth hth
   3.496 @@ -2093,9 +2095,9 @@
   3.497  	    val tnames = map fst tfrees
   3.498  	    val tsyn = mk_syn thy tycname
   3.499  	    val typ = (tycname,tnames,tsyn)
   3.500 -	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
   3.501 +	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
   3.502              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
   3.503 -				      
   3.504 +
   3.505  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
   3.506  
   3.507  	    val fulltyname = Sign.intern_type thy' tycname
   3.508 @@ -2124,11 +2126,11 @@
   3.509  	    val proc_prop = if null tnames
   3.510  			    then smart_string_of_cterm
   3.511  			    else Library.setmp show_all_types true smart_string_of_cterm
   3.512 -	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " 
   3.513 +	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
   3.514  				 ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
   3.515 -	    
   3.516 +
   3.517  	    val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
   3.518 -              
   3.519 +
   3.520  	    val _ = message "RESULT:"
   3.521  	    val _ = if_debug pth hth'
   3.522  	in
   3.523 @@ -2145,19 +2147,19 @@
   3.524          val eq = quote (constname ^ " == "^rhs)
   3.525  	val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
   3.526      in
   3.527 -	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy    
   3.528 +	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy
   3.529      end
   3.530  
   3.531 -fun add_dump_syntax thy name = 
   3.532 +fun add_dump_syntax thy name =
   3.533      let
   3.534        val n = quotename name
   3.535        val syn = string_of_mixfix (mk_syn thy name)
   3.536      in
   3.537        add_dump ("syntax\n  "^n^" :: _ "^syn) thy
   3.538      end
   3.539 -      
   3.540 +
   3.541  (*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
   3.542 -fun choose_upon_replay_history thy s dth = 
   3.543 +fun choose_upon_replay_history thy s dth =
   3.544      case Symtab.lookup (!type_intro_replay_history) s of
   3.545  	NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth)
   3.546        | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s))
   3.547 @@ -2167,7 +2169,7 @@
   3.548      case HOL4DefThy.get thy of
   3.549  	Replaying _ => (thy,
   3.550            HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth)
   3.551 -      | _ => 
   3.552 +      | _ =>
   3.553  	let
   3.554              val _ = message "TYPE_INTRO:"
   3.555  	    val _ = if_debug pth hth
   3.556 @@ -2192,9 +2194,9 @@
   3.557  	    val aty = Type (fulltyname, map mk_vartype tnames)
   3.558  	    val abs_ty = tT --> aty
   3.559  	    val rep_ty = aty --> tT
   3.560 -            val typedef_hol2hollight' = 
   3.561 -		Drule.instantiate' 
   3.562 -		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] 
   3.563 +            val typedef_hol2hollight' =
   3.564 +		Drule.instantiate'
   3.565 +		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
   3.566  		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
   3.567                      typedef_hol2hollight
   3.568  	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
   3.569 @@ -2209,7 +2211,7 @@
   3.570  	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
   3.571  	    val thy4 = add_hol4_pending thyname thmname args thy''
   3.572  	    val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   3.573 -	   
   3.574 +
   3.575  	    val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
   3.576  	    val c   =
   3.577  		let
   3.578 @@ -2217,27 +2219,27 @@
   3.579  		in
   3.580  		    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
   3.581  		end
   3.582 -	    
   3.583 +
   3.584  	    val tnames_string = if null tnames
   3.585  				then ""
   3.586  				else "(" ^ commas tnames ^ ") "
   3.587  	    val proc_prop = if null tnames
   3.588  			    then smart_string_of_cterm
   3.589  			    else Library.setmp show_all_types true smart_string_of_cterm
   3.590 -	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ 
   3.591 -              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ 
   3.592 +	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
   3.593 +              " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
   3.594  	      (string_of_mixfix tsyn) ^ " morphisms "^
   3.595 -              (quote rep_name)^" "^(quote abs_name)^"\n"^ 
   3.596 +              (quote rep_name)^" "^(quote abs_name)^"\n"^
   3.597  	      ("  apply (rule light_ex_imp_nonempty[where t="^
   3.598 -              (proc_prop (cterm_of thy4 t))^"])\n"^              
   3.599 +              (proc_prop (cterm_of thy4 t))^"])\n"^
   3.600  	      ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
   3.601  	    val str_aty = string_of_ctyp (ctyp_of thy aty)
   3.602 -            val thy = add_dump_syntax thy rep_name 
   3.603 +            val thy = add_dump_syntax thy rep_name
   3.604              val thy = add_dump_syntax thy abs_name
   3.605 -	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ 
   3.606 +	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
   3.607                " = typedef_hol2hollight \n"^
   3.608                "  [where a=\"a :: "^str_aty^"\" and r=r" ^
   3.609 -	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy 
   3.610 +	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
   3.611  	    val _ = message "RESULT:"
   3.612  	    val _ = if_debug pth hth'
   3.613  	in
     4.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 25 13:28:35 2007 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 25 13:28:37 2007 +0200
     4.3 @@ -380,10 +380,9 @@
     4.4  
     4.5  fun gen_primrec note def alt_name invs fctxt eqns thy =
     4.6    let
     4.7 -    fun readt T s = term_of (Thm.read_cterm thy (s, T));
     4.8      val ((names, strings), srcss) = apfst split_list (split_list eqns);
     4.9      val atts = map (map (Attrib.attribute thy)) srcss;
    4.10 -    val eqn_ts = map (fn s => readt propT s
    4.11 +    val eqn_ts = map (fn s => Syntax.read_prop_global thy s
    4.12        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
    4.13      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
    4.14        (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
    4.15 @@ -391,8 +390,8 @@
    4.16      val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts
    4.17    in
    4.18      gen_primrec_i note def alt_name
    4.19 -      (Option.map (map (readt dummyT)) invs)
    4.20 -      (Option.map (readt dummyT) fctxt)
    4.21 +      (Option.map (map (Syntax.read_term_global thy)) invs)
    4.22 +      (Option.map (Syntax.read_term_global thy) fctxt)
    4.23        (names ~~ eqn_ts' ~~ atts) thy
    4.24    end;
    4.25  
     5.1 --- a/src/HOL/Tools/TFL/post.ML	Tue Sep 25 13:28:35 2007 +0200
     5.2 +++ b/src/HOL/Tools/TFL/post.ML	Tue Sep 25 13:28:37 2007 +0200
     5.3 @@ -245,7 +245,8 @@
     5.4    in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
     5.5  
     5.6  fun define strict thy cs ss congs wfs fid R seqs =
     5.7 -  define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs)
     5.8 +  define_i strict thy cs ss congs wfs fid
     5.9 +      (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs)
    5.10      handle U.ERR {mesg,...} => error mesg;
    5.11  
    5.12  
    5.13 @@ -272,7 +273,7 @@
    5.14   end
    5.15  
    5.16  fun defer thy congs fid seqs =
    5.17 -  defer_i thy congs fid (map (Sign.read_term thy) seqs)
    5.18 +  defer_i thy congs fid (map (Syntax.read_term_global thy) seqs)
    5.19      handle U.ERR {mesg,...} => error mesg;
    5.20  end;
    5.21  
     6.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Sep 25 13:28:35 2007 +0200
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Sep 25 13:28:37 2007 +0200
     6.3 @@ -310,7 +310,7 @@
     6.4    let
     6.5      val ((names, strings), srcss) = apfst split_list (split_list eqns);
     6.6      val atts = map (map (Attrib.attribute thy)) srcss;
     6.7 -    val eqn_ts = map (fn s => term_of (Thm.read_cterm thy (s, propT))
     6.8 +    val eqn_ts = map (fn s => Syntax.read_prop_global thy s
     6.9        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
    6.10      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
    6.11        handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
     7.1 --- a/src/HOL/Tools/specification_package.ML	Tue Sep 25 13:28:35 2007 +0200
     7.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Sep 25 13:28:37 2007 +0200
     7.3 @@ -121,7 +121,7 @@
     7.4            | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
     7.5  
     7.6          val rew_imps = alt_props |>
     7.7 -          map (ObjectLogic.atomize o Thm.read_cterm thy o rpair Term.propT o snd)
     7.8 +          map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
     7.9          val props' = rew_imps |>
    7.10            map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
    7.11  
    7.12 @@ -144,7 +144,7 @@
    7.13          val thawed_prop_consts = collect_consts (prop_thawed,[])
    7.14          val (altcos,overloaded) = Library.split_list cos
    7.15          val (names,sconsts) = Library.split_list altcos
    7.16 -        val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts
    7.17 +        val consts = map (Syntax.read_term_global thy) sconsts
    7.18          val _ = not (Library.exists (not o Term.is_Const) consts)
    7.19            orelse error "Specification: Non-constant found as parameter"
    7.20  
     8.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Sep 25 13:28:35 2007 +0200
     8.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Sep 25 13:28:37 2007 +0200
     8.3 @@ -149,7 +149,7 @@
     8.4  fun hd_of (Const(a,_)) = a |
     8.5  hd_of (t $ _) = hd_of t |
     8.6  hd_of _ = raise malformed;
     8.7 -val trm = Sign.simple_read_term thy (Sign.read_typ thy atypstr) s;
     8.8 +val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
     8.9  in
    8.10  hd_of trm handle malformed =>
    8.11  error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
    8.12 @@ -330,10 +330,10 @@
    8.13  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
    8.14  let
    8.15  val state_type_string = type_product_of_varlist(statetupel);
    8.16 -val styp = Sign.read_typ thy state_type_string;
    8.17 +val styp = Syntax.read_typ_global thy state_type_string;
    8.18  val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
    8.19  val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
    8.20 -val atyp = Sign.read_typ thy action_type;
    8.21 +val atyp = Syntax.read_typ_global thy action_type;
    8.22  val inp_set_string = action_set_string thy atyp inp;
    8.23  val out_set_string = action_set_string thy atyp out;
    8.24  val int_set_string = action_set_string thy atyp int;
    8.25 @@ -426,7 +426,7 @@
    8.26  end)
    8.27  
    8.28  fun ren_act_type_of thy funct =
    8.29 -  (case Term.fastype_of (Sign.read_term thy funct) of
    8.30 +  (case Term.fastype_of (Syntax.read_term_global thy funct) of
    8.31      Type ("fun", [a, b]) => a
    8.32    | _ => error "could not extract argument type of renaming function term");
    8.33   
     9.1 --- a/src/HOLCF/Tools/cont_consts.ML	Tue Sep 25 13:28:35 2007 +0200
     9.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Tue Sep 25 13:28:37 2007 +0200
     9.3 @@ -91,7 +91,7 @@
     9.4      |> Sign.add_trrules_i (List.concat (map third transformed_decls))
     9.5    end;
     9.6  
     9.7 -val add_consts = gen_add_consts Sign.read_typ;
     9.8 +val add_consts = gen_add_consts Syntax.read_typ_global;
     9.9  val add_consts_i = gen_add_consts Sign.certify_typ;
    9.10  
    9.11  
    10.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Tue Sep 25 13:28:35 2007 +0200
    10.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Tue Sep 25 13:28:37 2007 +0200
    10.3 @@ -100,7 +100,7 @@
    10.4  fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
    10.5    let
    10.6      val dtnvs = map ((fn (dname,vs) => 
    10.7 -			 (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
    10.8 +			 (Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
    10.9                     o fst) eqs''';
   10.10      val cons''' = map snd eqs''';
   10.11      fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
   10.12 @@ -139,7 +139,7 @@
   10.13    end;
   10.14  
   10.15  val add_domain_i = gen_add_domain Sign.certify_typ;
   10.16 -val add_domain = gen_add_domain Sign.read_typ;
   10.17 +val add_domain = gen_add_domain Syntax.read_typ_global;
   10.18  
   10.19  
   10.20  (** outer syntax **)
    11.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 25 13:28:35 2007 +0200
    11.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 25 13:28:37 2007 +0200
    11.3 @@ -253,7 +253,7 @@
    11.4      else thy'
    11.5    end;
    11.6  
    11.7 -val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
    11.8 +val add_fixrec = gen_add_fixrec Syntax.read_prop_global Attrib.attribute;
    11.9  val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
   11.10  
   11.11  
   11.12 @@ -281,7 +281,7 @@
   11.13      (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   11.14    end;
   11.15  
   11.16 -val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
   11.17 +val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
   11.18  val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
   11.19  
   11.20  
    12.1 --- a/src/Provers/splitter.ML	Tue Sep 25 13:28:35 2007 +0200
    12.2 +++ b/src/Provers/splitter.ML	Tue Sep 25 13:28:37 2007 +0200
    12.3 @@ -103,8 +103,8 @@
    12.4  val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
    12.5  
    12.6  val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
    12.7 -  [Sign.read_prop Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
    12.8 -  (Sign.read_prop Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
    12.9 +  [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   12.10 +  (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
   12.11    (fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
   12.12  
   12.13  val trlift = lift RS transitive_thm;
    13.1 --- a/src/Pure/Isar/class.ML	Tue Sep 25 13:28:35 2007 +0200
    13.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 25 13:28:37 2007 +0200
    13.3 @@ -232,9 +232,10 @@
    13.4  
    13.5  local
    13.6  
    13.7 -fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =
    13.8 +fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
    13.9    let
   13.10 -    val (_, t) = read_def thy (raw_name, raw_t);
   13.11 +    val ctxt = ProofContext.init thy;
   13.12 +    val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
   13.13      val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
   13.14      val atts = map (prep_att thy) raw_atts;
   13.15      val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
   13.16 @@ -243,7 +244,7 @@
   13.17        | _ => SOME raw_name;
   13.18    in (c, (insts, ((name, t), atts))) end;
   13.19  
   13.20 -fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
   13.21 +fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
   13.22  fun read_def thy = gen_read_def thy (K I) (K I);
   13.23  
   13.24  fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
   13.25 @@ -544,9 +545,9 @@
   13.26  
   13.27  local
   13.28  
   13.29 -fun read_param thy raw_t =
   13.30 +fun read_param thy raw_t =  (* FIXME ProofContext.read_const (!?) *)
   13.31    let
   13.32 -    val t = Sign.read_term thy raw_t
   13.33 +    val t = Syntax.read_term_global thy raw_t
   13.34    in case try dest_Const t
   13.35     of SOME (c, _) => c
   13.36      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    14.1 --- a/src/Pure/Isar/code_unit.ML	Tue Sep 25 13:28:35 2007 +0200
    14.2 +++ b/src/Pure/Isar/code_unit.ML	Tue Sep 25 13:28:37 2007 +0200
    14.3 @@ -60,7 +60,7 @@
    14.4  
    14.5  fun read_bare_const thy raw_t =
    14.6    let
    14.7 -    val t = Sign.read_term thy raw_t;
    14.8 +    val t = Syntax.read_term_global thy raw_t;
    14.9    in case try dest_Const t
   14.10     of SOME c_ty => c_ty
   14.11      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    15.1 --- a/src/Pure/Proof/extraction.ML	Tue Sep 25 13:28:35 2007 +0200
    15.2 +++ b/src/Pure/Proof/extraction.ML	Tue Sep 25 13:28:37 2007 +0200
    15.3 @@ -213,7 +213,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 (Sign.read_prop thy' s)
    15.8 +    let val t = Logic.varify (Syntax.read_prop_global 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)
    16.1 --- a/src/Pure/codegen.ML	Tue Sep 25 13:28:35 2007 +0200
    16.2 +++ b/src/Pure/codegen.ML	Tue Sep 25 13:28:37 2007 +0200
    16.3 @@ -197,7 +197,7 @@
    16.4  
    16.5  fun set_default_type s thy ({size, iterations, ...} : test_params) =
    16.6    {size = size, iterations = iterations,
    16.7 -   default_type = SOME (Sign.read_typ thy s)};
    16.8 +   default_type = SOME (Syntax.read_typ_global thy s)};
    16.9  
   16.10  
   16.11  (* theory data *)
   16.12 @@ -1112,7 +1112,7 @@
   16.13      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   16.14       (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
   16.15         (fn ((name, mfx), aux) => (name, (parse_mixfix
   16.16 -         (Sign.read_typ thy) mfx, aux)))) xs thy)));
   16.17 +         (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
   16.18  
   16.19  val assoc_constP =
   16.20    OuterSyntax.command "consts_code"
   16.21 @@ -1171,7 +1171,7 @@
   16.22  
   16.23  fun parse_tyinst xs =
   16.24    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
   16.25 -    fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs;
   16.26 +    fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
   16.27  
   16.28  val test_paramsP =
   16.29    OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
    17.1 --- a/src/Pure/meta_simplifier.ML	Tue Sep 25 13:28:35 2007 +0200
    17.2 +++ b/src/Pure/meta_simplifier.ML	Tue Sep 25 13:28:37 2007 +0200
    17.3 @@ -646,7 +646,7 @@
    17.4  
    17.5  (* FIXME avoid global thy and Logic.varify *)
    17.6  fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
    17.7 -fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
    17.8 +fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
    17.9  
   17.10  
   17.11  local
    18.1 --- a/src/Pure/sign.ML	Tue Sep 25 13:28:35 2007 +0200
    18.2 +++ b/src/Pure/sign.ML	Tue Sep 25 13:28:37 2007 +0200
    18.3 @@ -492,7 +492,7 @@
    18.4    let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
    18.5    in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
    18.6  
    18.7 -val read_arity = prep_arity intern_type Syntax.global_read_sort;
    18.8 +val read_arity = prep_arity intern_type Syntax.read_sort_global;
    18.9  val cert_arity = prep_arity (K I) certify_sort;
   18.10  
   18.11  
   18.12 @@ -613,7 +613,7 @@
   18.13  fun gen_add_defsort prep_sort s thy =
   18.14    thy |> map_tsig (Type.set_defsort (prep_sort thy s));
   18.15  
   18.16 -val add_defsort = gen_add_defsort Syntax.global_read_sort;
   18.17 +val add_defsort = gen_add_defsort Syntax.read_sort_global;
   18.18  val add_defsort_i = gen_add_defsort certify_sort;
   18.19  
   18.20  
   18.21 @@ -650,12 +650,13 @@
   18.22      let
   18.23        val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
   18.24        val a' = Syntax.type_name a mx;
   18.25 -      val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (prep_typ thy rhs))
   18.26 +      val abbr = (a', vs,
   18.27 +          certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) rhs))
   18.28          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
   18.29        val tsig' = Type.add_abbrevs naming [abbr] tsig;
   18.30      in (naming, syn', tsig', consts) end);
   18.31  
   18.32 -val add_tyabbrs = fold (gen_add_tyabbr Syntax.global_parse_typ);
   18.33 +val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);
   18.34  val add_tyabbrs_i = fold (gen_add_tyabbr (K I));
   18.35  
   18.36  
   18.37 @@ -663,18 +664,19 @@
   18.38  
   18.39  fun gen_syntax change_gram prep_typ mode args thy =
   18.40    let
   18.41 -    fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (prep_typ thy T), mx)
   18.42 +    fun prep (c, T, mx) = (c,
   18.43 +        certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) T), mx)
   18.44        handle ERROR msg =>
   18.45          cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
   18.46    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
   18.47  
   18.48  fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
   18.49  
   18.50 -val add_modesyntax = gen_add_syntax Syntax.global_parse_typ;
   18.51 +val add_modesyntax = gen_add_syntax Syntax.parse_typ;
   18.52  val add_modesyntax_i = gen_add_syntax (K I);
   18.53  val add_syntax = add_modesyntax Syntax.default_mode;
   18.54  val add_syntax_i = add_modesyntax_i Syntax.default_mode;
   18.55 -val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.global_parse_typ;
   18.56 +val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
   18.57  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
   18.58  
   18.59  fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
    19.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Sep 25 13:28:35 2007 +0200
    19.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 25 13:28:37 2007 +0200
    19.3 @@ -335,7 +335,7 @@
    19.4      con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
    19.5    fun mk_free s =
    19.6      let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
    19.7 -      Goal.prove_global thy [] [] (Sign.read_prop thy s)
    19.8 +      Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
    19.9          (fn _ => EVERY
   19.10           [rewrite_goals_tac con_defs,
   19.11            fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
    20.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Sep 25 13:28:35 2007 +0200
    20.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Sep 25 13:28:37 2007 +0200
    20.3 @@ -197,7 +197,7 @@
    20.4  
    20.5  fun add_primrec args thy =
    20.6    add_primrec_i (map (fn ((name, s), srcs) =>
    20.7 -    ((name, Sign.read_prop thy s), map (Attrib.attribute thy) srcs))
    20.8 +    ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs))
    20.9      args) thy;
   20.10  
   20.11