# HG changeset patch # User clasohm # Date 794227685 -3600 # Node ID 196ca0973a6d679150ac86426aba621fb0347d7b # Parent 6bee3815c0bfe5d199a0b12e9ba312f2f8faceba added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure) diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/ROOT.ML Fri Mar 03 11:48:05 1995 +0100 @@ -65,6 +65,7 @@ open BasicSyntax Thm Drule Tactical Tactic Goals; structure Pure = struct val thy = pure_thy end; +structure CPure = struct val thy = cpure_thy end; (*Theory parser and loader*) cd "Thy"; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Syntax/ast.ML Fri Mar 03 11:48:05 1995 +0100 @@ -163,7 +163,6 @@ | unfold_ast_p _ y = ([], y); - (** normalization of asts **) (* tracing options *) diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Syntax/mixfix.ML Fri Mar 03 11:48:05 1995 +0100 @@ -139,8 +139,8 @@ val pure_types = map (fn t => (t, 0, NoSyn)) - (terminals @ [logic, "type", "types", "sort", "classes", args, "idt", - "idts", "aprop", "asms", any, sprop]); + (terminals @ [logic, "type", "types", "sort", "classes", args, + "idt", "idts", "aprop", "asms", any, sprop]); val pure_syntax = [("_lambda", "[idts, 'a] => logic", Mixfix ("(3%_./ _)", [], 0)), @@ -154,8 +154,6 @@ ("_idts", "[idt, idts] => idts", Mixfix ("_/ _", [1, 0], 0)), ("", "id => aprop", Delimfix "_"), ("", "var => aprop", Delimfix "_"), - (applC, "[('b => 'a), " ^ args ^ "] => aprop", - Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)), ("_aprop", "aprop => prop", Delimfix "PROP _"), ("", "prop => asms", Delimfix "_"), ("_asms", "[prop, asms] => asms", Delimfix "_;/ _"), @@ -163,7 +161,6 @@ ("_ofclass", "[type, logic] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), ("_K", "'a", NoSyn), ("", "id => logic", Delimfix "_"), - ("", "var => logic", Delimfix "_"), - ("_appl", "[logic, args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))] + ("", "var => logic", Delimfix "_")] end; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Syntax/printer.ML Fri Mar 03 11:48:05 1995 +0100 @@ -25,9 +25,9 @@ val empty_prtab: prtab val extend_prtab: prtab -> xprod list -> prtab val merge_prtabs: prtab -> prtab -> prtab - val pretty_term_ast: prtab -> (string -> (ast list -> ast) option) + val pretty_term_ast: bool -> prtab -> (string -> (ast list -> ast) option) -> ast -> Pretty.T - val pretty_typ_ast: prtab -> (string -> (ast list -> ast) option) + val pretty_typ_ast: bool -> prtab -> (string -> (ast list -> ast) option) -> ast -> Pretty.T end end; @@ -206,11 +206,12 @@ | chain [Arg _] = true | chain _ = false; -fun pretty prtab trf type_mode ast0 p0 = +fun pretty prtab trf type_mode curried ast0 p0 = let val trans = apply_trans "print ast translation"; - val appT = if type_mode then tappl_ast_tr' else appl_ast_tr'; + val appT = if type_mode then tappl_ast_tr' else + if curried then applC_ast_tr' else appl_ast_tr'; fun synT ([], args) = ([], args) | synT (Arg p :: symbs, t :: args) = @@ -221,7 +222,7 @@ val (Ts, args') = synT (symbs, args); in if type_mode then (astT (t, p) @ Ts, args') - else (pretty prtab trf true t p @ Ts, args') + else (pretty prtab trf true curried t p @ Ts, args') end | synT (String s :: symbs, args) = let val (Ts, args') = synT (symbs, args); @@ -281,14 +282,14 @@ (* pretty_term_ast *) -fun pretty_term_ast prtab trf ast = - Pretty.blk (0, pretty prtab trf false ast 0); +fun pretty_term_ast curried prtab trf ast = + Pretty.blk (0, pretty prtab trf false curried ast 0); (* pretty_typ_ast *) -fun pretty_typ_ast prtab trf ast = - Pretty.blk (0, pretty prtab trf true ast 0); +fun pretty_typ_ast _ prtab trf ast = + Pretty.blk (0, pretty prtab trf true false ast 0); end; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Fri Mar 03 11:48:05 1995 +0100 @@ -20,7 +20,6 @@ val args: string val any: string val sprop: string - val applC: string val typ_to_nonterm: typ -> string datatype xsymb = Delim of string | @@ -78,7 +77,6 @@ val logicT = Type (logic, []); val args = "args"; -val argsT = Type (args, []); val typeT = Type ("type", []); @@ -91,7 +89,6 @@ (* constants *) -val applC = "_appl"; val constrainC = "_constrain"; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Syntax/syn_trans.ML Fri Mar 03 11:48:05 1995 +0100 @@ -34,6 +34,7 @@ val abs_tr': term -> term val prop_tr': bool -> term -> term val appl_ast_tr': ast * ast list -> ast + val applC_ast_tr': ast * ast list -> ast val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast val ast_to_term: (string -> (term list -> term) option) -> ast -> term end @@ -51,8 +52,15 @@ (* application *) -fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args) - | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts; +fun appl_ast_tr [f, args] = Appl (f :: unfold_ast "_args" args) + | appl_ast_tr asts = raise_ast "appl_ast_tr" asts; + +fun applC_ast_tr [f, arg] = + let fun unfold_ast_c (y as Appl (Constant _ :: _)) = [y] + | unfold_ast_c (Appl xs) = xs + | unfold_ast_c y = [y]; + in Appl ((unfold_ast_c f) @ [arg]) end + | applC_ast_tr asts = raise_ast "applC_ast_tr" asts; (* abstraction *) @@ -124,6 +132,24 @@ fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f] | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args]; +fun applC_ast_tr' (f, []) = raise_ast "applC_ast_tr'" [f] + | applC_ast_tr' (f, arg::args) = + let (* fold curried function application *) + fun fold [] result = result + | fold (x :: xs) result = + fold xs (Appl [Constant "_applC", result, x]); + in fold args (Appl [Constant "_applC", f, arg]) end; +(* + f a b c () + ("_applC" f a) + + b c ("_applC" f a) + ("_applC" ("_applC" f a) b) + + c ("_applC" ("_applC" f a) b) + ("_applC" ("_applC" ("_applC" f a) b) c) +*) + (* abstraction *) @@ -253,9 +279,11 @@ (** pure_trfuns **) val pure_trfuns = - ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), - ("_bigimpl", bigimpl_ast_tr)], - [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), ("_K", k_tr)], + ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr), + ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), + ("_bigimpl", bigimpl_ast_tr)], + [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), + ("_K", k_tr)], [], [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr')]); diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Syntax/syntax.ML Fri Mar 03 11:48:05 1995 +0100 @@ -54,9 +54,9 @@ val read: syntax -> typ -> string -> term list val read_typ: syntax -> (indexname -> sort) -> string -> typ val simple_read_typ: string -> typ - val pretty_term: syntax -> term -> Pretty.T + val pretty_term: bool -> syntax -> term -> Pretty.T val pretty_typ: syntax -> typ -> Pretty.T - val string_of_term: syntax -> term -> string + val string_of_term: bool -> syntax -> term -> string val string_of_typ: syntax -> typ -> string val simple_string_of_typ: typ -> string val simple_pprint_typ: typ -> pprint_args -> unit @@ -403,19 +403,20 @@ (** pretty terms or typs **) -fun pretty_t t_to_ast pretty_t (syn as Syntax tabs) t = +fun pretty_t t_to_ast pretty_t curried (syn as Syntax tabs) t = let val {print_trtab, print_ruletab, print_ast_trtab, prtab, ...} = tabs; val ast = t_to_ast (lookup_trtab print_trtab) t; in - pretty_t prtab (lookup_trtab print_ast_trtab) + pretty_t curried prtab (lookup_trtab print_ast_trtab) (normalize_ast (lookup_ruletab print_ruletab) ast) end; val pretty_term = pretty_t term_to_ast pretty_term_ast; -val pretty_typ = pretty_t typ_to_ast pretty_typ_ast; +val pretty_typ = pretty_t typ_to_ast pretty_typ_ast false; -fun string_of_term syn t = Pretty.string_of (pretty_term syn t); +fun string_of_term curried syn t = + Pretty.string_of (pretty_term curried syn t); fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty); val simple_string_of_typ = string_of_typ type_syn; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/Thy/thy_read.ML Fri Mar 03 11:48:05 1995 +0100 @@ -57,9 +57,20 @@ datatype basetype = Thy of string | File of string; -val loaded_thys = ref (Symtab.make [("Pure", ThyInfo {path = "", children = [], +val loaded_thys = ref (Symtab.make [("ProtoPure", + ThyInfo {path = "", + children = ["Pure", "CPure"], + thy_time = Some "", ml_time = Some "", + theory = Some proto_pure_thy, + thms = Symtab.null}), + ("Pure", ThyInfo {path = "", children = [], thy_time = Some "", ml_time = Some "", theory = Some pure_thy, + thms = Symtab.null}), + ("CPure", ThyInfo {path = "", + children = [], + thy_time = Some "", ml_time = Some "", + theory = Some cpure_thy, thms = Symtab.null})]); val loadpath = ref ["."]; (*default search path for theory files *) @@ -91,10 +102,8 @@ fun already_loaded thy = let val t = get_thyinfo thy in if is_none t then false - else let val ThyInfo {thy_time, ml_time, ...} = the t - in if is_none thy_time orelse is_none ml_time then false - else true - end + else let val ThyInfo {theory, ...} = the t + in if is_none theory then false else true end end; (*Check if a theory file has changed since its last use. @@ -323,21 +332,21 @@ end | reload_changed [] = (); - (*Remove all theories that are no descendants of Pure. + (*Remove all theories that are no descendants of ProtoPure. If there are still children in the deleted theory's list schedule them for reloading *) fun collect_garbage not_garbage = let fun collect ((tname, ThyInfo {children, ...}) :: ts) = if tname mem not_garbage then collect ts - else (writeln ("Theory \"" ^ tname - ^ "\" is no longer linked with Pure - removing it."); + else (writeln ("Theory \"" ^ tname ^ + "\" is no longer linked with ProtoPure - removing it."); remove_thy tname; seq mark_outdated children) | collect [] = () in collect (Symtab.dest (!loaded_thys)) end; - in collect_garbage ("Pure" :: (load_order ["Pure"] [])); - reload_changed (load_order ["Pure"] []) + in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] [])); + reload_changed (load_order ["Pure", "CPure"] []) end; (*Merge theories to build a base for a new theory. @@ -413,7 +422,7 @@ b :: (load_base bs)) | load_base (File b :: bs) = (load b; - load_base bs) (*don't add it to merge_theories' parameter *) + load_base bs) (*don't add it to mergelist *) | load_base [] = []; (*Get theory object for a loaded theory *) @@ -435,7 +444,7 @@ thy_time = thy_time, ml_time = ml_time, theory = Some thy, thms = thms} | None => ThyInfo {path = "", children = [], - thy_time = Some "", ml_time = Some "", + thy_time = None, ml_time = None, theory = Some thy, thms = Symtab.null}; in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/drule.ML Fri Mar 03 11:48:05 1995 +0100 @@ -421,9 +421,7 @@ (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts); in (show_no_free_types := true; show_sorts := false; - Pretty.writeln (pretty_term B); - if ngoals = 0 then writeln "No subgoals!" else if ngoals > maxgoals then (print_goals (1, take (maxgoals, As)); @@ -640,22 +638,22 @@ val reflexive_thm = - let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),logicS))) + let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS))) in Thm.reflexive cx end; val symmetric_thm = - let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT) + let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; val transitive_thm = - let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT) - val yz = read_cterm Sign.pure ("y::'a::logic == z",propT) + let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT) + val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT) val xythm = Thm.assume xy and yzthm = Thm.assume yz in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; (** Below, a "conversion" has type cterm -> thm **) -val refl_cimplies = reflexive (cterm_of Sign.pure implies); +val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies); (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) (*Do not rewrite flex-flex pairs*) @@ -734,17 +732,17 @@ (*** Some useful meta-theorems ***) (*The rule V/V, obtains assumption solving for eresolve_tac*) -val asm_rl = trivial(read_cterm Sign.pure ("PROP ?psi",propT)); +val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT)); (*Meta-level cut rule: [| V==>W; V |] ==> W *) -val cut_rl = trivial(read_cterm Sign.pure +val cut_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi ==> PROP ?theta", propT)); (*Generalized elim rule for one conclusion; cut_rl with reversed premises: [| PROP V; PROP V ==> PROP W |] ==> PROP W *) val revcut_rl = - let val V = read_cterm Sign.pure ("PROP V", propT) - and VW = read_cterm Sign.pure ("PROP V ==> PROP W", propT); + let val V = read_cterm Sign.proto_pure ("PROP V", propT) + and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT); in standard (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) @@ -752,16 +750,16 @@ (*for deleting an unwanted assumption*) val thin_rl = - let val V = read_cterm Sign.pure ("PROP V", propT) - and W = read_cterm Sign.pure ("PROP W", propT); + let val V = read_cterm Sign.proto_pure ("PROP V", propT) + and W = read_cterm Sign.proto_pure ("PROP W", propT); in standard (implies_intr V (implies_intr W (assume W))) end; (* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) val triv_forall_equality = - let val V = read_cterm Sign.pure ("PROP V", propT) - and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT) - and x = read_cterm Sign.pure ("x", TFree("'a",logicS)); + let val V = read_cterm Sign.proto_pure ("PROP V", propT) + and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT) + and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS)); in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) (implies_intr V (forall_intr x (assume V)))) end; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/goals.ML --- a/src/Pure/goals.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/goals.ML Fri Mar 03 11:48:05 1995 +0100 @@ -100,7 +100,7 @@ ref((fn _=> error"No goal has been supplied in subgoal module") : bool*thm->thm); -val dummy = trivial(read_cterm Sign.pure +val dummy = trivial(read_cterm Sign.proto_pure ("PROP No_goal_has_been_supplied",propT)); (*List of previous goal stacks, for the undo operation. Set by setstate. diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/sign.ML Fri Mar 03 11:48:05 1995 +0100 @@ -61,7 +61,9 @@ val add_name: string -> sg -> sg val make_draft: sg -> sg val merge: sg * sg -> sg + val proto_pure: sg val pure: sg + val cpure: sg val const_of_class: class -> string val class_of_const: string -> class end @@ -179,10 +181,16 @@ (** pretty printing of terms and types **) -fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn; +fun pretty_term (Sg {syn, stamps, ...}) = + let val curried = "CPure" mem (map ! stamps); + in Syntax.pretty_term curried syn end; + fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn; -fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn; +fun string_of_term (Sg {syn, stamps, ...}) = + let val curried = "CPure" mem (map ! stamps); + in Syntax.string_of_term curried syn end; + fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn; fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg); @@ -516,7 +524,7 @@ (** the Pure signature **) -val pure = +val proto_pure = make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#" |> add_types (("fun", 2, NoSyn) :: @@ -537,7 +545,24 @@ ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)), ("all", "('a => prop) => prop", Binder ("!!", 0, 0)), ("TYPE", "'a itself", NoSyn)] + |> add_name "ProtoPure"; + +val pure = proto_pure + |> add_syntax + [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", + [max_pri, 0], max_pri)), + ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", + [max_pri, 0], max_pri))] |> add_name "Pure"; +val cpure = proto_pure + |> add_syntax + [("_applC", "[('b => 'a), 'c] => logic", Mixfix ("(1_ (1_))", + [max_pri-1, max_pri], + max_pri-1)), + ("_applC", "[('b => 'a), 'c] => aprop", Mixfix ("(1_ (1_))", + [max_pri-1, max_pri], + max_pri-1))] + |> add_name "CPure"; end; diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/tactic.ML --- a/src/Pure/tactic.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/tactic.ML Fri Mar 03 11:48:05 1995 +0100 @@ -238,7 +238,7 @@ increment revcut_rl instead.*) fun make_elim_preserve rl = let val {maxidx,...} = rep_thm rl - fun cvar ixn = cterm_of Sign.pure (Var(ixn,propT)); + fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT)); val revcut_rl' = instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/tctical.ML --- a/src/Pure/tctical.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/tctical.ML Fri Mar 03 11:48:05 1995 +0100 @@ -437,7 +437,7 @@ (* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) val dummy_quant_rl = standard (forall_elim_var 0 (assume - (read_cterm Sign.pure ("!!x::prop. PROP V",propT)))); + (read_cterm Sign.proto_pure ("!!x::prop. PROP V",propT)))); (* Prevent the subgoal's assumptions from becoming additional subgoals in the new proof state by enclosing them by a universal quantification *) diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/thm.ML Fri Mar 03 11:48:05 1995 +0100 @@ -101,7 +101,9 @@ val parents_of : theory -> theory list val prems_of : thm -> term list val prems_of_mss : meta_simpset -> thm list + val proto_pure_thy : theory val pure_thy : theory + val cpure_thy : theory val read_def_cterm : Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> string * typ -> cterm * (indexname * typ) list @@ -294,11 +296,17 @@ (Symtab.dest (#new_axioms (rep_theory thy))); -(* the Pure theory *) +(* the Pure theories *) + +val proto_pure_thy = + Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []}; val pure_thy = Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []}; +val cpure_thy = + Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []}; + (** extend theory **) @@ -398,7 +406,7 @@ | (None, false) => Theory { sign = (if mk_draft then Sign.make_draft else I) - (foldl add_sign (Sign.pure, thys)), + (foldl add_sign (Sign.proto_pure, thys)), new_axioms = Symtab.null, parents = thys}) end; @@ -496,9 +504,9 @@ (*Definition of the relation =?= *) val flexpair_def = - Thm{sign= Sign.pure, hyps= [], maxidx= 0, + Thm{sign= Sign.proto_pure, hyps= [], maxidx= 0, prop= term_of - (read_cterm Sign.pure + (read_cterm Sign.proto_pure ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}; (*The reflexivity rule: maps t to the theorem t==t *) diff -r 6bee3815c0bf -r 196ca0973a6d src/Pure/unify.ML --- a/src/Pure/unify.ML Thu Mar 02 12:07:20 1995 +0100 +++ b/src/Pure/unify.ML Fri Mar 03 11:48:05 1995 +0100 @@ -53,7 +53,7 @@ and trace_types = ref false (*announce potential incompleteness of type unification*) -val sgr = ref(Sign.pure); +val sgr = ref(Sign.proto_pure); type binderlist = (string*typ) list;