--- 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";
--- 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 *)
--- 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;
--- 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;
--- 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";
--- 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')]);
--- 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;
--- 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;
--- 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;
--- 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.
--- 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;
--- 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
--- 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 *)
--- 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 *)
--- 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;