# HG changeset patch # User wenzelm # Date 1190719717 -7200 # Node ID dfeb98f84e93bf4dba325cca20e15b322796a213 # Parent c58547ff329bbbd9c071655b29e8be102f51c3bc Syntax.parse/check/read; diff -r c58547ff329b -r dfeb98f84e93 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/FOLP/simp.ML Tue Sep 25 13:28:37 2007 +0200 @@ -594,7 +594,7 @@ let fun readfT(f,s) = let - val T = Logic.incr_tvar 9 (Sign.read_typ thy s); + val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s); val t = case Sign.const_type thy f of SOME(_) => Const(f,T) | NONE => Free(f,T) in (t,T) end diff -r c58547ff329b -r dfeb98f84e93 src/HOL/Import/import_syntax.ML --- a/src/HOL/Import/import_syntax.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOL/Import/import_syntax.ML Tue Sep 25 13:28:37 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 (Sign.read_typ thy ty) thy) (thy,constmaps) + | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global 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 (Sign.read_typ thy ty) thy) (thy,constmaps) + | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps) end) fun import_thy s = diff -r c58547ff329b -r dfeb98f84e93 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOL/Import/proof_kernel.ML Tue Sep 25 13:28:37 2007 +0200 @@ -10,7 +10,7 @@ type term type thm type ('a,'b) subst - + type proof_info datatype proof = Proof of proof_info * proof_content and proof_content @@ -111,8 +111,8 @@ val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm val new_axiom : string -> term -> theory -> theory * thm - val prin : term -> unit - val protect_factname : string -> string + val prin : term -> unit + val protect_factname : string -> string val replay_protect_varname : string -> string -> unit val replay_add_dump : string -> theory -> theory end @@ -125,7 +125,7 @@ type ('a,'b) subst = ('a * 'b) list datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm -fun hthm2thm (HOLThm (_, th)) = th +fun hthm2thm (HOLThm (_, th)) = th fun to_hol_thm th = HOLThm ([], th) @@ -134,7 +134,7 @@ datatype proof_info = Info of {disk_info: (string * string) option ref} - + datatype proof = Proof of proof_info * proof_content and proof_content = PRefl of term @@ -176,7 +176,7 @@ exception PK of string * string fun ERR f mesg = PK (f,mesg) -fun print_exn e = +fun print_exn e = case e of PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e) | _ => OldGoals.print_exn e @@ -213,21 +213,23 @@ fun smart_string_of_cterm ct = let val {thy,t,T,...} = rep_cterm ct + val ctxt = ProofContext.init thy (* Hack to avoid parse errors with Trueprop *) val ct = (cterm_of thy (HOLogic.dest_Trueprop t) handle TERM _ => ct) - fun match cu = t aconv (term_of cu) + fun match u = t aconv u fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true) | G 1 = Library.setmp show_brackets true (G 0) | G 2 = Library.setmp show_all_types true (G 0) | G 3 = Library.setmp show_brackets true (G 2) - | G _ = raise SMART_STRING + | G _ = raise SMART_STRING fun F n = let val str = Library.setmp show_brackets false (G n string_of_cterm) ct - val cu = Thm.read_cterm thy (str,T) + val u = Syntax.parse_term ctxt str + |> TypeInfer.constrain T |> Syntax.check_term ctxt in - if match cu + if match u then quote str else F (n+1) end @@ -237,7 +239,7 @@ PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0 end handle ERROR mesg => simple_smart_string_of_cterm ct - + val smart_string_of_thm = smart_string_of_cterm o cprop_of fun prth th = writeln (PrintMode.setmp [] string_of_thm th) @@ -272,20 +274,20 @@ in F end -fun i mem L = - let fun itr [] = false - | itr (a::rst) = i=a orelse itr rst +fun i mem L = + let fun itr [] = false + | itr (a::rst) = i=a orelse itr rst in itr L end; - + fun insert i L = if i mem L then L else i::L - + fun mk_set [] = [] | mk_set (a::rst) = insert a (mk_set rst) - + fun [] union S = S | S union [] = S | (a::rst) union S2 = rst union (insert a S2) - + fun implode_subst [] = [] | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest)) | implode_subst _ = raise ERR "implode_subst" "malformed substitution list" @@ -300,7 +302,7 @@ fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2)) end -(* Acutal code. *) +(* Actual code. *) fun get_segment thyname l = (Lib.assoc "s" l handle PK _ => thyname) @@ -430,8 +432,8 @@ fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) -local - fun get_const sg thyname name = +local + fun get_const sg thyname name = (case Sign.const_type sg name of SOME ty => Const (name, ty) | NONE => raise ERR "get_type" (name ^ ": No such constant")) @@ -472,16 +474,16 @@ val check_name_thy = theory "Main" fun valid_boundvarname s = - can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) (); + can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) (); fun valid_varname s = - can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) (); + can (fn () => Syntax.read_term_global check_name_thy s) (); fun protect_varname s = if innocent_varname s andalso valid_varname s then s else case Symtab.lookup (!protected_varnames) s of SOME t => t - | NONE => + | NONE => let val _ = inc invented_isavar val t = "u_" ^ string_of_int (!invented_isavar) @@ -493,56 +495,56 @@ exception REPLAY_PROTECT_VARNAME of string*string*string -fun replay_protect_varname s t = +fun replay_protect_varname s t = case Symtab.lookup (!protected_varnames) s of SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') - | NONE => + | NONE => let val _ = inc invented_isavar val t = "u_" ^ string_of_int (!invented_isavar) val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) in () - end - + end + fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u" fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) | mk_lambda v t = raise TERM ("lambda", [v, t]); - -fun replacestr x y s = + +fun replacestr x y s = let val xl = explode x val yl = explode y fun isprefix [] ys = true | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false - | isprefix _ _ = false + | isprefix _ _ = false fun isp s = isprefix xl s fun chg s = yl@(List.drop (s, List.length xl)) fun r [] = [] - | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) + | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) in implode(r (explode s)) -end +end fun protect_factname s = replacestr "." "_dot_" s -fun unprotect_factname s = replacestr "_dot_" "." s +fun unprotect_factname s = replacestr "_dot_" "." s val ty_num_prefix = "N_" fun startsWithDigit s = Char.isDigit (hd (String.explode s)) -fun protect_tyname tyn = +fun protect_tyname tyn = let - val tyn' = - if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else + val tyn' = + if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else (if startsWithDigit tyn then ty_num_prefix^tyn else tyn) in tyn' end -fun protect_constname tcn = tcn +fun protect_constname tcn = tcn (* if tcn = ".." then "dotdot" else if tcn = "==" then "eqeq" else tcn*) @@ -634,9 +636,9 @@ in mk_comb(f,a) end - | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = - let - val x = get_term_from_index thy thyname types terms tmx + | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = + let + val x = get_term_from_index thy thyname types terms tmx val a = get_term_from_index thy thyname types terms tma in mk_lambda x a @@ -683,7 +685,7 @@ in Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path) end - + fun proof_file_name thyname thmname thy = let val path = case get_proof_dir thyname thy of @@ -693,7 +695,7 @@ in OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}} end - + fun xml_to_proof thyname types terms prf thy = let val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types @@ -936,18 +938,18 @@ x2p prf end -fun import_proof_concl thyname thmname thy = +fun import_proof_concl thyname thmname thy = let val is = TextIO.openIn(proof_file_name thyname thmname thy) val (proof_xml,_) = scan_tag (LazySeq.of_instream is) val _ = TextIO.closeIn is - in + in case proof_xml of Elem("proof",[],xtypes::xterms::prf::rest) => let val types = TypeNet.input_types thyname xtypes val terms = TermNet.input_terms thyname types xterms - fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm + fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm in case rest of [] => NONE @@ -962,7 +964,7 @@ val is = TextIO.openIn(proof_file_name thyname thmname thy) val (proof_xml,_) = scan_tag (LazySeq.of_instream is) val _ = TextIO.closeIn is - in + in case proof_xml of Elem("proof",[],xtypes::xterms::prf::rest) => let @@ -1068,7 +1070,7 @@ res end -val permute_prems = Thm.permute_prems +val permute_prems = Thm.permute_prems fun rearrange sg tm th = let @@ -1152,26 +1154,26 @@ | name_of _ = ERR "name_of" fun new_name' bump map n = let val n' = n^bump in - if is_old_name n' orelse Symtab.lookup map n' <> NONE then + if is_old_name n' orelse Symtab.lookup map n' <> NONE then new_name' (Symbol.bump_string bump) map n else n' - end + end val new_name = new_name' "a" fun replace_name n' (Free (n, t)) = Free (n', t) | replace_name n' _ = ERR "replace_name" - (* map: old or fresh name -> old free, + (* map: old or fresh name -> old free, invmap: old free which has fresh name assigned to it -> fresh name *) fun dis (v, mapping as (map,invmap)) = let val n = name_of v in case Symtab.lookup map n of NONE => (Symtab.update (n, v) map, invmap) - | SOME v' => - if v=v' then - mapping + | SOME v' => + if v=v' then + mapping else let val n' = new_name map n in - (Symtab.update (n', v) map, + (Symtab.update (n', v) map, Termtab.update (v, n') invmap) end end @@ -1179,16 +1181,16 @@ if (length freenames = length frees) then thm else - let - val (_, invmap) = - List.foldl dis (Symtab.empty, Termtab.empty) frees + let + val (_, invmap) = + List.foldl dis (Symtab.empty, Termtab.empty) frees fun make_subst ((oldfree, newname), (intros, elims)) = - (cterm_of thy oldfree :: intros, + (cterm_of thy oldfree :: intros, cterm_of thy (replace_name newname oldfree) :: elims) val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap) - in + in forall_elim_list elims (forall_intr_list intros thm) - end + end end val debug = ref false @@ -1201,7 +1203,7 @@ fun get_hol4_thm thyname thmname thy = case get_hol4_theorem thyname thmname thy of SOME hth => SOME (HOLThm hth) - | NONE => + | NONE => let val pending = HOL4Pending.get thy in @@ -1215,7 +1217,7 @@ c = "All" orelse c = "op -->" orelse c = "op &" orelse - c = "op =")) (Term.term_consts tm) + c = "op =")) (Term.term_consts tm) fun match_consts t (* th *) = let @@ -1291,7 +1293,7 @@ end | SOME NONE => error ("Trying to access ignored theorem " ^ thmname) | NONE => - let + let val _ = (message "Looking for conclusion:"; if_debug prin isaconc) val cs = non_trivial_term_consts isaconc @@ -1325,7 +1327,7 @@ val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) in case concl_of i2h_conc of - Const("==",_) $ lhs $ _ => + Const("==",_) $ lhs $ _ => (warning ("Failed lookup of theorem '"^thmname^"':"); writeln "Original conclusion:"; prin hol4conc'; @@ -1334,10 +1336,10 @@ | _ => () end in - case b of + case b of NONE => (warn () handle _ => (); (a,b)) | _ => (a, b) - end + end fun get_thm thyname thmname thy = case get_hol4_thm thyname thmname thy of @@ -1373,11 +1375,11 @@ val rew = rewrite_hol4_term (concl_of th) thy val th = equal_elim rew th val thy' = add_hol4_pending thyname thmname args thy - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val th = disambiguate_frees th val thy2 = if gen_output - then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ - (smart_string_of_thm th) ^ "\n by (import " ^ + then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ + (smart_string_of_thm th) ^ "\n by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")") thy' else thy' in @@ -1768,7 +1770,7 @@ in (thy,res) end - + fun CCONTR tm hth thy = let @@ -1851,7 +1853,7 @@ end) th vlist' end | SOME _ => raise ERR "GEN_ABS" "Bad constant" - | NONE => + | NONE => foldr (fn (v,th) => mk_ABS v th thy) th vlist' val res = HOLThm(rens_of info',th1) val _ = message "RESULT:" @@ -1947,7 +1949,7 @@ val p3 = string_of_mixfix csyn val p4 = smart_string_of_cterm crhs in - add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' + add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' end else (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ @@ -1958,7 +1960,7 @@ | NONE => raise ERR "new_definition" "Bad conclusion" val fullname = Sign.full_name thy22 thmname val thy22' = case opt_get_output_thy thy22 of - "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; + "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; add_hol4_mapping thyname thmname fullname thy22) | output_thy => let @@ -1982,7 +1984,7 @@ fun new_specification thyname thmname names hth thy = case HOL4DefThy.get thy of Replaying _ => (thy,hth) - | _ => + | _ => let val _ = message "NEW_SPEC:" val _ = if_debug pth hth @@ -2005,7 +2007,7 @@ dest_eta_abs abody | dest_exists tm = raise ERR "new_specification" "Bad existential formula" - + val (consts,_) = Library.foldl (fn ((cs,ex),cname) => let val (_,cT,p) = dest_exists ex @@ -2056,11 +2058,11 @@ intern_store_thm false thyname thmname hth thy'' end handle e => (message "exception in new_specification"; print_exn e) - + end - + fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")") - + fun to_isa_thm (hth as HOLThm(_,th)) = let val (HOLThm args) = norm_hthm (theory_of_thm th) hth @@ -2079,7 +2081,7 @@ fun new_type_definition thyname thmname tycname hth thy = case HOL4DefThy.get thy of Replaying _ => (thy,hth) - | _ => + | _ => let val _ = message "TYPE_DEF:" val _ = if_debug pth hth @@ -2093,9 +2095,9 @@ val tnames = map fst tfrees val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 - + val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 val fulltyname = Sign.intern_type thy' tycname @@ -2124,11 +2126,11 @@ val proc_prop = if null tnames then smart_string_of_cterm else Library.setmp show_all_types true smart_string_of_cterm - val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " + val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4 - + val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5 - + val _ = message "RESULT:" val _ = if_debug pth hth' in @@ -2145,19 +2147,19 @@ val eq = quote (constname ^ " == "^rhs) val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : " in - add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy + add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy end -fun add_dump_syntax thy name = +fun add_dump_syntax thy name = let val n = quotename name val syn = string_of_mixfix (mk_syn thy name) in add_dump ("syntax\n "^n^" :: _ "^syn) thy end - + (*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table) -fun choose_upon_replay_history thy s dth = +fun choose_upon_replay_history thy s dth = case Symtab.lookup (!type_intro_replay_history) s of NONE => (type_intro_replay_history := Symtab.update (s, ()) (!type_intro_replay_history); dth) | SOME _ => HOLThm([], PureThy.get_thm thy (PureThy.Name s)) @@ -2167,7 +2169,7 @@ case HOL4DefThy.get thy of Replaying _ => (thy, HOLThm([], PureThy.get_thm thy (PureThy.Name (thmname^"_@intern"))) handle ERROR _ => hth) - | _ => + | _ => let val _ = message "TYPE_INTRO:" val _ = if_debug pth hth @@ -2192,9 +2194,9 @@ val aty = Type (fulltyname, map mk_vartype tnames) val abs_ty = tT --> aty val rep_ty = aty --> tT - val typedef_hol2hollight' = - Drule.instantiate' - [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] + val typedef_hol2hollight' = + Drule.instantiate' + [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] typedef_hol2hollight val th4 = (#type_definition typedef_info) RS typedef_hol2hollight' @@ -2209,7 +2211,7 @@ val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) val thy4 = add_hol4_pending thyname thmname args thy'' val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') - + val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *) val c = let @@ -2217,27 +2219,27 @@ in Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P' end - + val tnames_string = if null tnames then "" else "(" ^ commas tnames ^ ") " val proc_prop = if null tnames then smart_string_of_cterm else Library.setmp show_all_types true smart_string_of_cterm - val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ - " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ + val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ + " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ (string_of_mixfix tsyn) ^ " morphisms "^ - (quote rep_name)^" "^(quote abs_name)^"\n"^ + (quote rep_name)^" "^(quote abs_name)^"\n"^ (" apply (rule light_ex_imp_nonempty[where t="^ - (proc_prop (cterm_of thy4 t))^"])\n"^ + (proc_prop (cterm_of thy4 t))^"])\n"^ (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 val str_aty = string_of_ctyp (ctyp_of thy aty) - val thy = add_dump_syntax thy rep_name + val thy = add_dump_syntax thy rep_name val thy = add_dump_syntax thy abs_name - val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ + val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight \n"^ " [where a=\"a :: "^str_aty^"\" and r=r" ^ - " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy + " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy val _ = message "RESULT:" val _ = if_debug pth hth' in diff -r c58547ff329b -r dfeb98f84e93 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 13:28:37 2007 +0200 @@ -380,10 +380,9 @@ fun gen_primrec note def alt_name invs fctxt eqns thy = let - fun readt T s = term_of (Thm.read_cterm thy (s, T)); val ((names, strings), srcss) = apfst split_list (split_list eqns); val atts = map (map (Attrib.attribute thy)) srcss; - val eqn_ts = map (fn s => readt propT s + val eqn_ts = map (fn s => Syntax.read_prop_global thy s handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings; val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq)))) @@ -391,8 +390,8 @@ val (_, eqn_ts') = PrimrecPackage.unify_consts thy rec_ts eqn_ts in gen_primrec_i note def alt_name - (Option.map (map (readt dummyT)) invs) - (Option.map (readt dummyT) fctxt) + (Option.map (map (Syntax.read_term_global thy)) invs) + (Option.map (Syntax.read_term_global thy) fctxt) (names ~~ eqn_ts' ~~ atts) thy end; diff -r c58547ff329b -r dfeb98f84e93 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOL/Tools/TFL/post.ML Tue Sep 25 13:28:37 2007 +0200 @@ -245,7 +245,8 @@ in (thy, {rules = rules', induct = induct, tcs = tcs}) end; fun define strict thy cs ss congs wfs fid R seqs = - define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs) + define_i strict thy cs ss congs wfs fid + (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs) handle U.ERR {mesg,...} => error mesg; @@ -272,7 +273,7 @@ end fun defer thy congs fid seqs = - defer_i thy congs fid (map (Sign.read_term thy) seqs) + defer_i thy congs fid (map (Syntax.read_term_global thy) seqs) handle U.ERR {mesg,...} => error mesg; end; diff -r c58547ff329b -r dfeb98f84e93 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOL/Tools/primrec_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -310,7 +310,7 @@ let val ((names, strings), srcss) = apfst split_list (split_list eqns); val atts = map (map (Attrib.attribute thy)) srcss; - val eqn_ts = map (fn s => term_of (Thm.read_cterm thy (s, propT)) + val eqn_ts = map (fn s => Syntax.read_prop_global thy s handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings; val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq))) handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts; diff -r c58547ff329b -r dfeb98f84e93 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOL/Tools/specification_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -121,7 +121,7 @@ | myfoldr f [] = error "SpecificationPackage.process_spec internal error" val rew_imps = alt_props |> - map (ObjectLogic.atomize o Thm.read_cterm thy o rpair Term.propT o snd) + map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd) val props' = rew_imps |> map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) @@ -144,7 +144,7 @@ val thawed_prop_consts = collect_consts (prop_thawed,[]) val (altcos,overloaded) = Library.split_list cos val (names,sconsts) = Library.split_list altcos - val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts + val consts = map (Syntax.read_term_global thy) sconsts val _ = not (Library.exists (not o Term.is_Const) consts) orelse error "Specification: Non-constant found as parameter" diff -r c58547ff329b -r dfeb98f84e93 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -149,7 +149,7 @@ fun hd_of (Const(a,_)) = a | hd_of (t $ _) = hd_of t | hd_of _ = raise malformed; -val trm = Sign.simple_read_term thy (Sign.read_typ thy atypstr) s; +val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; in hd_of trm handle malformed => error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) @@ -330,10 +330,10 @@ (writeln("Constructing automaton " ^ automaton_name ^ " ..."); let val state_type_string = type_product_of_varlist(statetupel); -val styp = Sign.read_typ thy state_type_string; +val styp = Syntax.read_typ_global 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 = Sign.read_typ thy action_type; +val atyp = Syntax.read_typ_global 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; @@ -426,7 +426,7 @@ end) fun ren_act_type_of thy funct = - (case Term.fastype_of (Sign.read_term thy funct) of + (case Term.fastype_of (Syntax.read_term_global thy funct) of Type ("fun", [a, b]) => a | _ => error "could not extract argument type of renaming function term"); diff -r c58547ff329b -r dfeb98f84e93 src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOLCF/Tools/cont_consts.ML Tue Sep 25 13:28:37 2007 +0200 @@ -91,7 +91,7 @@ |> Sign.add_trrules_i (List.concat (map third transformed_decls)) end; -val add_consts = gen_add_consts Sign.read_typ; +val add_consts = gen_add_consts Syntax.read_typ_global; val add_consts_i = gen_add_consts Sign.certify_typ; diff -r c58547ff329b -r dfeb98f84e93 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Tue Sep 25 13:28:37 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 (Sign.read_typ thy''') vs)) + (Sign.full_name thy''' dname, map (Syntax.read_typ_global 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 Sign.read_typ; +val add_domain = gen_add_domain Syntax.read_typ_global; (** outer syntax **) diff -r c58547ff329b -r dfeb98f84e93 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/HOLCF/Tools/fixrec_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -253,7 +253,7 @@ else thy' end; -val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute; +val add_fixrec = gen_add_fixrec Syntax.read_prop_global Attrib.attribute; val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I); @@ -281,7 +281,7 @@ (snd o PureThy.add_thmss [((name, simps), atts)]) thy end; -val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute; +val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute; val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I); diff -r c58547ff329b -r dfeb98f84e93 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Provers/splitter.ML Tue Sep 25 13:28:37 2007 +0200 @@ -103,8 +103,8 @@ val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; (* (P == Q) ==> Q ==> P *) val lift = Goal.prove_global Pure.thy ["P", "Q", "R"] - [Sign.read_prop Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"] - (Sign.read_prop Pure.thy "P(%x. Q(x)) == P(%x. R(x))") + [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"] + (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))") (fn [prem] => rewtac prem THEN rtac reflexive_thm 1) val trlift = lift RS transitive_thm; diff -r c58547ff329b -r dfeb98f84e93 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Pure/Isar/class.ML Tue Sep 25 13:28:37 2007 +0200 @@ -232,9 +232,10 @@ local -fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) = +fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) = let - val (_, t) = read_def thy (raw_name, raw_t); + val ctxt = ProofContext.init thy; + val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt; val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t; val atts = map (prep_att thy) raw_atts; val insts = Consts.typargs (Sign.consts_of thy) (c, ty); @@ -243,7 +244,7 @@ | _ => SOME raw_name; in (c, (insts, ((name, t), atts))) end; -fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm; +fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop; fun read_def thy = gen_read_def thy (K I) (K I); fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory = @@ -544,9 +545,9 @@ local -fun read_param thy raw_t = +fun read_param thy raw_t = (* FIXME ProofContext.read_const (!?) *) let - val t = Sign.read_term thy raw_t + val t = Syntax.read_term_global thy raw_t in case try dest_Const t of SOME (c, _) => c | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) diff -r c58547ff329b -r dfeb98f84e93 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Pure/Isar/code_unit.ML Tue Sep 25 13:28:37 2007 +0200 @@ -60,7 +60,7 @@ fun read_bare_const thy raw_t = let - val t = Sign.read_term thy raw_t; + val t = Syntax.read_term_global thy raw_t; in case try dest_Const t of SOME c_ty => c_ty | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) diff -r c58547ff329b -r dfeb98f84e93 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Sep 25 13:28:37 2007 +0200 @@ -213,7 +213,7 @@ fun read_condeq thy = let val thy' = add_syntax thy in fn s => - let val t = Logic.varify (Sign.read_prop thy' s) + let val t = Logic.varify (Syntax.read_prop_global 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) diff -r c58547ff329b -r dfeb98f84e93 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Pure/codegen.ML Tue Sep 25 13:28:37 2007 +0200 @@ -197,7 +197,7 @@ fun set_default_type s thy ({size, iterations, ...} : test_params) = {size = size, iterations = iterations, - default_type = SOME (Sign.read_typ thy s)}; + default_type = SOME (Syntax.read_typ_global thy s)}; (* theory data *) @@ -1112,7 +1112,7 @@ (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> (fn xs => Toplevel.theory (fn thy => fold (assoc_type o (fn ((name, mfx), aux) => (name, (parse_mixfix - (Sign.read_typ thy) mfx, aux)))) xs thy))); + (Syntax.read_typ_global thy) mfx, aux)))) xs thy))); val assoc_constP = OuterSyntax.command "consts_code" @@ -1171,7 +1171,7 @@ fun parse_tyinst xs = (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy => - fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs; + fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs; val test_paramsP = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl diff -r c58547ff329b -r dfeb98f84e93 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Pure/meta_simplifier.ML Tue Sep 25 13:28:37 2007 +0200 @@ -646,7 +646,7 @@ (* FIXME avoid global thy and Logic.varify *) fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify); -fun simproc thy name = simproc_i thy name o map (Sign.read_term thy); +fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy); local diff -r c58547ff329b -r dfeb98f84e93 src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/Pure/sign.ML Tue Sep 25 13:28:37 2007 +0200 @@ -492,7 +492,7 @@ let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S) in Type.add_arity (pp thy) arity (tsig_of thy); arity end; -val read_arity = prep_arity intern_type Syntax.global_read_sort; +val read_arity = prep_arity intern_type Syntax.read_sort_global; val cert_arity = prep_arity (K I) certify_sort; @@ -613,7 +613,7 @@ fun gen_add_defsort prep_sort s thy = thy |> map_tsig (Type.set_defsort (prep_sort thy s)); -val add_defsort = gen_add_defsort Syntax.global_read_sort; +val add_defsort = gen_add_defsort Syntax.read_sort_global; val add_defsort_i = gen_add_defsort certify_sort; @@ -650,12 +650,13 @@ let val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn; val a' = Syntax.type_name a mx; - val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (prep_typ thy rhs)) + val abbr = (a', vs, + certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) rhs)) handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a'); val tsig' = Type.add_abbrevs naming [abbr] tsig; in (naming, syn', tsig', consts) end); -val add_tyabbrs = fold (gen_add_tyabbr Syntax.global_parse_typ); +val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ); val add_tyabbrs_i = fold (gen_add_tyabbr (K I)); @@ -663,18 +664,19 @@ fun gen_syntax change_gram prep_typ mode args thy = let - fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (prep_typ thy T), mx) + fun prep (c, T, mx) = (c, + certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) T), mx) handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx)); in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end; fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x; -val add_modesyntax = gen_add_syntax Syntax.global_parse_typ; +val add_modesyntax = gen_add_syntax Syntax.parse_typ; val add_modesyntax_i = gen_add_syntax (K I); val add_syntax = add_modesyntax Syntax.default_mode; val add_syntax_i = add_modesyntax_i Syntax.default_mode; -val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.global_parse_typ; +val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ; val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I); fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx) diff -r c58547ff329b -r dfeb98f84e93 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/ZF/Tools/datatype_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -335,7 +335,7 @@ con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) fun mk_free s = let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*) - Goal.prove_global thy [] [] (Sign.read_prop thy s) + Goal.prove_global thy [] [] (Syntax.read_prop_global thy s) (fn _ => EVERY [rewrite_goals_tac con_defs, fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]) diff -r c58547ff329b -r dfeb98f84e93 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Sep 25 13:28:35 2007 +0200 +++ b/src/ZF/Tools/primrec_package.ML Tue Sep 25 13:28:37 2007 +0200 @@ -197,7 +197,7 @@ fun add_primrec args thy = add_primrec_i (map (fn ((name, s), srcs) => - ((name, Sign.read_prop thy s), map (Attrib.attribute thy) srcs)) + ((name, Syntax.read_prop_global thy s), map (Attrib.attribute thy) srcs)) args) thy;