added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
authorclasohm
Fri Mar 03 11:48:05 1995 +0100 (1995-03-03)
changeset 922196ca0973a6d
parent 921 6bee3815c0bf
child 923 ff1574a81019
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
src/Pure/ROOT.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thy_read.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/thm.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 02 12:07:20 1995 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Mar 03 11:48:05 1995 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4  open BasicSyntax Thm Drule Tactical Tactic Goals;
     1.5  
     1.6  structure Pure = struct val thy = pure_thy end;
     1.7 +structure CPure = struct val thy = cpure_thy end;
     1.8  
     1.9  (*Theory parser and loader*)
    1.10  cd "Thy";
     2.1 --- a/src/Pure/Syntax/ast.ML	Thu Mar 02 12:07:20 1995 +0100
     2.2 +++ b/src/Pure/Syntax/ast.ML	Fri Mar 03 11:48:05 1995 +0100
     2.3 @@ -163,7 +163,6 @@
     2.4    | unfold_ast_p _ y = ([], y);
     2.5  
     2.6  
     2.7 -
     2.8  (** normalization of asts **)
     2.9  
    2.10  (* tracing options *)
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Mar 02 12:07:20 1995 +0100
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Mar 03 11:48:05 1995 +0100
     3.3 @@ -139,8 +139,8 @@
     3.4  
     3.5  val pure_types =
     3.6    map (fn t => (t, 0, NoSyn))
     3.7 -    (terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
     3.8 -      "idts", "aprop", "asms", any, sprop]);
     3.9 +    (terminals @ [logic, "type", "types", "sort", "classes", args,
    3.10 +      "idt", "idts", "aprop", "asms", any, sprop]);
    3.11  
    3.12  val pure_syntax =
    3.13   [("_lambda",   "[idts, 'a] => logic",            Mixfix ("(3%_./ _)", [], 0)),
    3.14 @@ -154,8 +154,6 @@
    3.15    ("_idts",     "[idt, idts] => idts",            Mixfix ("_/ _", [1, 0], 0)),
    3.16    ("",          "id => aprop",                    Delimfix "_"),
    3.17    ("",          "var => aprop",                   Delimfix "_"),
    3.18 -  (applC,       "[('b => 'a), " ^ args ^ "] => aprop",
    3.19 -    Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
    3.20    ("_aprop",    "aprop => prop",                  Delimfix "PROP _"),
    3.21    ("",          "prop => asms",                   Delimfix "_"),
    3.22    ("_asms",     "[prop, asms] => asms",           Delimfix "_;/ _"),
    3.23 @@ -163,7 +161,6 @@
    3.24    ("_ofclass",  "[type, logic] => prop",          Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    3.25    ("_K",        "'a",                             NoSyn),
    3.26    ("",          "id => logic",                    Delimfix "_"),
    3.27 -  ("",          "var => logic",                   Delimfix "_"),
    3.28 -  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))]
    3.29 +  ("",          "var => logic",                   Delimfix "_")]
    3.30  
    3.31  end;
     4.1 --- a/src/Pure/Syntax/printer.ML	Thu Mar 02 12:07:20 1995 +0100
     4.2 +++ b/src/Pure/Syntax/printer.ML	Fri Mar 03 11:48:05 1995 +0100
     4.3 @@ -25,9 +25,9 @@
     4.4      val empty_prtab: prtab
     4.5      val extend_prtab: prtab -> xprod list -> prtab
     4.6      val merge_prtabs: prtab -> prtab -> prtab
     4.7 -    val pretty_term_ast: prtab -> (string -> (ast list -> ast) option)
     4.8 +    val pretty_term_ast: bool -> prtab -> (string -> (ast list -> ast) option)
     4.9        -> ast -> Pretty.T
    4.10 -    val pretty_typ_ast: prtab -> (string -> (ast list -> ast) option)
    4.11 +    val pretty_typ_ast: bool -> prtab -> (string -> (ast list -> ast) option)
    4.12        -> ast -> Pretty.T
    4.13    end
    4.14  end;
    4.15 @@ -206,11 +206,12 @@
    4.16    | chain [Arg _] = true
    4.17    | chain _  = false;
    4.18  
    4.19 -fun pretty prtab trf type_mode ast0 p0 =
    4.20 +fun pretty prtab trf type_mode curried ast0 p0 =
    4.21    let
    4.22      val trans = apply_trans "print ast translation";
    4.23  
    4.24 -    val appT = if type_mode then tappl_ast_tr' else appl_ast_tr';
    4.25 +    val appT = if type_mode then tappl_ast_tr' else
    4.26 +               if curried then applC_ast_tr' else appl_ast_tr';
    4.27  
    4.28      fun synT ([], args) = ([], args)
    4.29        | synT (Arg p :: symbs, t :: args) =
    4.30 @@ -221,7 +222,7 @@
    4.31              val (Ts, args') = synT (symbs, args);
    4.32            in
    4.33              if type_mode then (astT (t, p) @ Ts, args')
    4.34 -            else (pretty prtab trf true t p @ Ts, args')
    4.35 +            else (pretty prtab trf true curried t p @ Ts, args')
    4.36            end
    4.37        | synT (String s :: symbs, args) =
    4.38            let val (Ts, args') = synT (symbs, args);
    4.39 @@ -281,14 +282,14 @@
    4.40  
    4.41  (* pretty_term_ast *)
    4.42  
    4.43 -fun pretty_term_ast prtab trf ast =
    4.44 -  Pretty.blk (0, pretty prtab trf false ast 0);
    4.45 +fun pretty_term_ast curried prtab trf ast =
    4.46 +  Pretty.blk (0, pretty prtab trf false curried ast 0);
    4.47  
    4.48  
    4.49  (* pretty_typ_ast *)
    4.50  
    4.51 -fun pretty_typ_ast prtab trf ast =
    4.52 -  Pretty.blk (0, pretty prtab trf true ast 0);
    4.53 +fun pretty_typ_ast _ prtab trf ast =
    4.54 +  Pretty.blk (0, pretty prtab trf true false ast 0);
    4.55  
    4.56  
    4.57  end;
     5.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Mar 02 12:07:20 1995 +0100
     5.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Mar 03 11:48:05 1995 +0100
     5.3 @@ -20,7 +20,6 @@
     5.4      val args: string
     5.5      val any: string
     5.6      val sprop: string
     5.7 -    val applC: string
     5.8      val typ_to_nonterm: typ -> string
     5.9      datatype xsymb =
    5.10        Delim of string |
    5.11 @@ -78,7 +77,6 @@
    5.12  val logicT = Type (logic, []);
    5.13  
    5.14  val args = "args";
    5.15 -val argsT = Type (args, []);
    5.16  
    5.17  val typeT = Type ("type", []);
    5.18  
    5.19 @@ -91,7 +89,6 @@
    5.20  
    5.21  (* constants *)
    5.22  
    5.23 -val applC = "_appl";
    5.24  val constrainC = "_constrain";
    5.25  
    5.26  
     6.1 --- a/src/Pure/Syntax/syn_trans.ML	Thu Mar 02 12:07:20 1995 +0100
     6.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Mar 03 11:48:05 1995 +0100
     6.3 @@ -34,6 +34,7 @@
     6.4      val abs_tr': term -> term
     6.5      val prop_tr': bool -> term -> term
     6.6      val appl_ast_tr': ast * ast list -> ast
     6.7 +    val applC_ast_tr': ast * ast list -> ast
     6.8      val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
     6.9      val ast_to_term: (string -> (term list -> term) option) -> ast -> term
    6.10    end
    6.11 @@ -51,8 +52,15 @@
    6.12  
    6.13  (* application *)
    6.14  
    6.15 -fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args)
    6.16 -  | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts;
    6.17 +fun appl_ast_tr [f, args] = Appl (f :: unfold_ast "_args" args)
    6.18 +  | appl_ast_tr asts = raise_ast "appl_ast_tr" asts;
    6.19 +
    6.20 +fun applC_ast_tr [f, arg] =
    6.21 +      let fun unfold_ast_c (y as Appl (Constant _ :: _)) = [y]
    6.22 +            | unfold_ast_c (Appl xs) = xs
    6.23 +            | unfold_ast_c y = [y];
    6.24 +      in Appl ((unfold_ast_c f) @ [arg]) end
    6.25 +  | applC_ast_tr asts = raise_ast "applC_ast_tr" asts;
    6.26  
    6.27  
    6.28  (* abstraction *)
    6.29 @@ -124,6 +132,24 @@
    6.30  fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]
    6.31    | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
    6.32  
    6.33 +fun applC_ast_tr' (f, []) = raise_ast "applC_ast_tr'" [f]
    6.34 +  | applC_ast_tr' (f, arg::args) =
    6.35 +      let (* fold curried function application *)
    6.36 +          fun fold [] result = result
    6.37 +            | fold (x :: xs) result =
    6.38 +                fold xs (Appl [Constant "_applC", result, x]);
    6.39 +      in fold args (Appl [Constant "_applC", f, arg]) end;
    6.40 +(*
    6.41 +        f a b c  ()
    6.42 +        ("_applC" f a)
    6.43 +
    6.44 +        b c      ("_applC" f a)
    6.45 +	("_applC" ("_applC" f a) b)
    6.46 +
    6.47 +        c	 ("_applC" ("_applC" f a) b)
    6.48 +	("_applC" ("_applC" ("_applC" f a) b) c)
    6.49 +*)
    6.50 +
    6.51  
    6.52  (* abstraction *)
    6.53  
    6.54 @@ -253,9 +279,11 @@
    6.55  (** pure_trfuns **)
    6.56  
    6.57  val pure_trfuns =
    6.58 - ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
    6.59 -    ("_bigimpl", bigimpl_ast_tr)],
    6.60 -  [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), ("_K", k_tr)],
    6.61 + ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
    6.62 +   ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
    6.63 +   ("_bigimpl", bigimpl_ast_tr)],
    6.64 +  [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    6.65 +   ("_K", k_tr)],
    6.66    [],
    6.67    [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr')]);
    6.68  
     7.1 --- a/src/Pure/Syntax/syntax.ML	Thu Mar 02 12:07:20 1995 +0100
     7.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Mar 03 11:48:05 1995 +0100
     7.3 @@ -54,9 +54,9 @@
     7.4    val read: syntax -> typ -> string -> term list
     7.5    val read_typ: syntax -> (indexname -> sort) -> string -> typ
     7.6    val simple_read_typ: string -> typ
     7.7 -  val pretty_term: syntax -> term -> Pretty.T
     7.8 +  val pretty_term: bool -> syntax -> term -> Pretty.T
     7.9    val pretty_typ: syntax -> typ -> Pretty.T
    7.10 -  val string_of_term: syntax -> term -> string
    7.11 +  val string_of_term: bool -> syntax -> term -> string
    7.12    val string_of_typ: syntax -> typ -> string
    7.13    val simple_string_of_typ: typ -> string
    7.14    val simple_pprint_typ: typ -> pprint_args -> unit
    7.15 @@ -403,19 +403,20 @@
    7.16  
    7.17  (** pretty terms or typs **)
    7.18  
    7.19 -fun pretty_t t_to_ast pretty_t (syn as Syntax tabs) t =
    7.20 +fun pretty_t t_to_ast pretty_t curried (syn as Syntax tabs) t =
    7.21    let
    7.22      val {print_trtab, print_ruletab, print_ast_trtab, prtab, ...} = tabs;
    7.23      val ast = t_to_ast (lookup_trtab print_trtab) t;
    7.24    in
    7.25 -    pretty_t prtab (lookup_trtab print_ast_trtab)
    7.26 +    pretty_t curried prtab (lookup_trtab print_ast_trtab)
    7.27        (normalize_ast (lookup_ruletab print_ruletab) ast)
    7.28    end;
    7.29  
    7.30  val pretty_term = pretty_t term_to_ast pretty_term_ast;
    7.31 -val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
    7.32 +val pretty_typ = pretty_t typ_to_ast pretty_typ_ast false;
    7.33  
    7.34 -fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
    7.35 +fun string_of_term curried syn t =
    7.36 +  Pretty.string_of (pretty_term curried syn t);
    7.37  fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
    7.38  
    7.39  val simple_string_of_typ = string_of_typ type_syn;
     8.1 --- a/src/Pure/Thy/thy_read.ML	Thu Mar 02 12:07:20 1995 +0100
     8.2 +++ b/src/Pure/Thy/thy_read.ML	Fri Mar 03 11:48:05 1995 +0100
     8.3 @@ -57,9 +57,20 @@
     8.4  datatype basetype = Thy  of string
     8.5                    | File of string;
     8.6  
     8.7 -val loaded_thys = ref (Symtab.make [("Pure", ThyInfo {path = "", children = [],
     8.8 +val loaded_thys = ref (Symtab.make [("ProtoPure",
     8.9 +                                     ThyInfo {path = "",
    8.10 +                                       children = ["Pure", "CPure"],
    8.11 +                                       thy_time = Some "", ml_time = Some "",
    8.12 +                                       theory = Some proto_pure_thy,
    8.13 +                                       thms = Symtab.null}),
    8.14 +                                    ("Pure", ThyInfo {path = "", children = [],
    8.15                                         thy_time = Some "", ml_time = Some "",
    8.16                                         theory = Some pure_thy,
    8.17 +                                       thms = Symtab.null}),
    8.18 +                                    ("CPure", ThyInfo {path = "",
    8.19 +                                       children = [],
    8.20 +                                       thy_time = Some "", ml_time = Some "",
    8.21 +                                       theory = Some cpure_thy,
    8.22                                         thms = Symtab.null})]);
    8.23  
    8.24  val loadpath = ref ["."];           (*default search path for theory files *)
    8.25 @@ -91,10 +102,8 @@
    8.26  fun already_loaded thy =
    8.27    let val t = get_thyinfo thy
    8.28    in if is_none t then false
    8.29 -     else let val ThyInfo {thy_time, ml_time, ...} = the t
    8.30 -          in if is_none thy_time orelse is_none ml_time then false
    8.31 -             else true
    8.32 -          end
    8.33 +     else let val ThyInfo {theory, ...} = the t
    8.34 +          in if is_none theory then false else true end
    8.35    end;
    8.36  
    8.37  (*Check if a theory file has changed since its last use.
    8.38 @@ -323,21 +332,21 @@
    8.39              end
    8.40          | reload_changed [] = ();
    8.41  
    8.42 -     (*Remove all theories that are no descendants of Pure.
    8.43 +     (*Remove all theories that are no descendants of ProtoPure.
    8.44         If there are still children in the deleted theory's list
    8.45         schedule them for reloading *)
    8.46       fun collect_garbage not_garbage =
    8.47         let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
    8.48                   if tname mem not_garbage then collect ts
    8.49 -                 else (writeln ("Theory \"" ^ tname
    8.50 -                         ^ "\" is no longer linked with Pure - removing it.");
    8.51 +                 else (writeln ("Theory \"" ^ tname ^
    8.52 +                       "\" is no longer linked with ProtoPure - removing it.");
    8.53                         remove_thy tname;
    8.54                         seq mark_outdated children)
    8.55               | collect [] = ()
    8.56  
    8.57         in collect (Symtab.dest (!loaded_thys)) end;
    8.58 -  in collect_garbage ("Pure" :: (load_order ["Pure"] []));
    8.59 -     reload_changed (load_order ["Pure"] [])
    8.60 +  in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
    8.61 +     reload_changed (load_order ["Pure", "CPure"] [])
    8.62    end;
    8.63  
    8.64  (*Merge theories to build a base for a new theory.
    8.65 @@ -413,7 +422,7 @@
    8.66                  b :: (load_base bs))
    8.67              | load_base (File b :: bs) =
    8.68                 (load b;
    8.69 -                load_base bs)    (*don't add it to merge_theories' parameter *)
    8.70 +                load_base bs)                    (*don't add it to mergelist *)
    8.71              | load_base [] = [];
    8.72  
    8.73            (*Get theory object for a loaded theory *)
    8.74 @@ -435,7 +444,7 @@
    8.75                            thy_time = thy_time, ml_time = ml_time,
    8.76                            theory = Some thy, thms = thms}
    8.77               | None => ThyInfo {path = "", children = [],
    8.78 -                                thy_time = Some "", ml_time = Some "",
    8.79 +                                thy_time = None, ml_time = None,
    8.80                                  theory = Some thy, thms = Symtab.null};
    8.81    in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
    8.82  
     9.1 --- a/src/Pure/drule.ML	Thu Mar 02 12:07:20 1995 +0100
     9.2 +++ b/src/Pure/drule.ML	Fri Mar 03 11:48:05 1995 +0100
     9.3 @@ -421,9 +421,7 @@
     9.4        (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
     9.5    in
     9.6      (show_no_free_types := true; show_sorts := false;
     9.7 -
     9.8        Pretty.writeln (pretty_term B);
     9.9 -
    9.10        if ngoals = 0 then writeln "No subgoals!"
    9.11        else if ngoals > maxgoals then
    9.12          (print_goals (1, take (maxgoals, As));
    9.13 @@ -640,22 +638,22 @@
    9.14  
    9.15  
    9.16  val reflexive_thm =
    9.17 -  let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),logicS)))
    9.18 +  let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
    9.19    in Thm.reflexive cx end;
    9.20  
    9.21  val symmetric_thm =
    9.22 -  let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
    9.23 +  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
    9.24    in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
    9.25  
    9.26  val transitive_thm =
    9.27 -  let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
    9.28 -      val yz = read_cterm Sign.pure ("y::'a::logic == z",propT)
    9.29 +  let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
    9.30 +      val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
    9.31        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    9.32    in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    9.33  
    9.34  (** Below, a "conversion" has type cterm -> thm **)
    9.35  
    9.36 -val refl_cimplies = reflexive (cterm_of Sign.pure implies);
    9.37 +val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
    9.38  
    9.39  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
    9.40  (*Do not rewrite flex-flex pairs*)
    9.41 @@ -734,17 +732,17 @@
    9.42  (*** Some useful meta-theorems ***)
    9.43  
    9.44  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    9.45 -val asm_rl = trivial(read_cterm Sign.pure ("PROP ?psi",propT));
    9.46 +val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
    9.47  
    9.48  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    9.49 -val cut_rl = trivial(read_cterm Sign.pure
    9.50 +val cut_rl = trivial(read_cterm Sign.proto_pure
    9.51          ("PROP ?psi ==> PROP ?theta", propT));
    9.52  
    9.53  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
    9.54       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
    9.55  val revcut_rl =
    9.56 -  let val V = read_cterm Sign.pure ("PROP V", propT)
    9.57 -      and VW = read_cterm Sign.pure ("PROP V ==> PROP W", propT);
    9.58 +  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
    9.59 +      and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
    9.60    in  standard (implies_intr V
    9.61                  (implies_intr VW
    9.62                   (implies_elim (assume VW) (assume V))))
    9.63 @@ -752,16 +750,16 @@
    9.64  
    9.65  (*for deleting an unwanted assumption*)
    9.66  val thin_rl =
    9.67 -  let val V = read_cterm Sign.pure ("PROP V", propT)
    9.68 -      and W = read_cterm Sign.pure ("PROP W", propT);
    9.69 +  let val V = read_cterm Sign.proto_pure ("PROP V", propT)
    9.70 +      and W = read_cterm Sign.proto_pure ("PROP W", propT);
    9.71    in  standard (implies_intr V (implies_intr W (assume W)))
    9.72    end;
    9.73  
    9.74  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
    9.75  val triv_forall_equality =
    9.76 -  let val V  = read_cterm Sign.pure ("PROP V", propT)
    9.77 -      and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
    9.78 -      and x  = read_cterm Sign.pure ("x", TFree("'a",logicS));
    9.79 +  let val V  = read_cterm Sign.proto_pure ("PROP V", propT)
    9.80 +      and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
    9.81 +      and x  = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
    9.82    in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
    9.83                             (implies_intr V  (forall_intr x (assume V))))
    9.84    end;
    10.1 --- a/src/Pure/goals.ML	Thu Mar 02 12:07:20 1995 +0100
    10.2 +++ b/src/Pure/goals.ML	Fri Mar 03 11:48:05 1995 +0100
    10.3 @@ -100,7 +100,7 @@
    10.4      ref((fn _=> error"No goal has been supplied in subgoal module") 
    10.5         : bool*thm->thm);
    10.6  
    10.7 -val dummy = trivial(read_cterm Sign.pure 
    10.8 +val dummy = trivial(read_cterm Sign.proto_pure 
    10.9      ("PROP No_goal_has_been_supplied",propT));
   10.10  
   10.11  (*List of previous goal stacks, for the undo operation.  Set by setstate. 
    11.1 --- a/src/Pure/sign.ML	Thu Mar 02 12:07:20 1995 +0100
    11.2 +++ b/src/Pure/sign.ML	Fri Mar 03 11:48:05 1995 +0100
    11.3 @@ -61,7 +61,9 @@
    11.4      val add_name: string -> sg -> sg
    11.5      val make_draft: sg -> sg
    11.6      val merge: sg * sg -> sg
    11.7 +    val proto_pure: sg
    11.8      val pure: sg
    11.9 +    val cpure: sg
   11.10      val const_of_class: class -> string
   11.11      val class_of_const: string -> class
   11.12    end
   11.13 @@ -179,10 +181,16 @@
   11.14  
   11.15  (** pretty printing of terms and types **)
   11.16  
   11.17 -fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
   11.18 +fun pretty_term (Sg {syn, stamps, ...}) =
   11.19 +  let val curried = "CPure" mem (map ! stamps);
   11.20 +  in Syntax.pretty_term curried syn end;
   11.21 +
   11.22  fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
   11.23  
   11.24 -fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
   11.25 +fun string_of_term (Sg {syn, stamps, ...}) = 
   11.26 +  let val curried = "CPure" mem (map ! stamps);
   11.27 +  in Syntax.string_of_term curried syn end;
   11.28 +
   11.29  fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
   11.30  
   11.31  fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   11.32 @@ -516,7 +524,7 @@
   11.33  
   11.34  (** the Pure signature **)
   11.35  
   11.36 -val pure =
   11.37 +val proto_pure =
   11.38    make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#"
   11.39    |> add_types
   11.40     (("fun", 2, NoSyn) ::
   11.41 @@ -537,7 +545,24 @@
   11.42      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
   11.43      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   11.44      ("TYPE", "'a itself", NoSyn)]
   11.45 +  |> add_name "ProtoPure";
   11.46 +
   11.47 +val pure = proto_pure
   11.48 +  |> add_syntax
   11.49 +   [("_appl",     "[('b => 'a), args] => logic",    Mixfix ("(1_/(1'(_')))",
   11.50 +                                                    [max_pri, 0], max_pri)),
   11.51 +    ("_appl",     "[('b => 'a), args] => aprop",    Mixfix ("(1_/(1'(_')))",
   11.52 +                                                    [max_pri, 0], max_pri))]
   11.53    |> add_name "Pure";
   11.54  
   11.55 +val cpure = proto_pure
   11.56 +  |> add_syntax
   11.57 +   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("(1_ (1_))",
   11.58 +                                                    [max_pri-1, max_pri],
   11.59 +                                                    max_pri-1)),
   11.60 +    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("(1_ (1_))",
   11.61 +                                                    [max_pri-1, max_pri],
   11.62 +                                                    max_pri-1))]
   11.63 +  |> add_name "CPure";
   11.64  
   11.65  end;
    12.1 --- a/src/Pure/tactic.ML	Thu Mar 02 12:07:20 1995 +0100
    12.2 +++ b/src/Pure/tactic.ML	Fri Mar 03 11:48:05 1995 +0100
    12.3 @@ -238,7 +238,7 @@
    12.4    increment revcut_rl instead.*)
    12.5  fun make_elim_preserve rl = 
    12.6    let val {maxidx,...} = rep_thm rl
    12.7 -      fun cvar ixn = cterm_of Sign.pure (Var(ixn,propT));
    12.8 +      fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
    12.9        val revcut_rl' = 
   12.10  	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   12.11  			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    13.1 --- a/src/Pure/tctical.ML	Thu Mar 02 12:07:20 1995 +0100
    13.2 +++ b/src/Pure/tctical.ML	Fri Mar 03 11:48:05 1995 +0100
    13.3 @@ -437,7 +437,7 @@
    13.4  (* (!!x. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
    13.5  val dummy_quant_rl = 
    13.6    standard (forall_elim_var 0 (assume 
    13.7 -                  (read_cterm Sign.pure ("!!x::prop. PROP V",propT))));
    13.8 +                  (read_cterm Sign.proto_pure ("!!x::prop. PROP V",propT))));
    13.9  
   13.10  (* Prevent the subgoal's assumptions from becoming additional subgoals in the
   13.11     new proof state by enclosing them by a universal quantification *)
    14.1 --- a/src/Pure/thm.ML	Thu Mar 02 12:07:20 1995 +0100
    14.2 +++ b/src/Pure/thm.ML	Fri Mar 03 11:48:05 1995 +0100
    14.3 @@ -101,7 +101,9 @@
    14.4    val parents_of	: theory -> theory list
    14.5    val prems_of		: thm -> term list
    14.6    val prems_of_mss	: meta_simpset -> thm list
    14.7 +  val proto_pure_thy	: theory
    14.8    val pure_thy		: theory
    14.9 +  val cpure_thy		: theory
   14.10    val read_def_cterm 	:
   14.11           Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
   14.12           string * typ -> cterm * (indexname * typ) list
   14.13 @@ -294,11 +296,17 @@
   14.14      (Symtab.dest (#new_axioms (rep_theory thy)));
   14.15  
   14.16  
   14.17 -(* the Pure theory *)
   14.18 +(* the Pure theories *)
   14.19 +
   14.20 +val proto_pure_thy =
   14.21 +  Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []};
   14.22  
   14.23  val pure_thy =
   14.24    Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []};
   14.25  
   14.26 +val cpure_thy =
   14.27 +  Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []};
   14.28 +
   14.29  
   14.30  
   14.31  (** extend theory **)
   14.32 @@ -398,7 +406,7 @@
   14.33      | (None, false) => Theory {
   14.34          sign =
   14.35            (if mk_draft then Sign.make_draft else I)
   14.36 -          (foldl add_sign (Sign.pure, thys)),
   14.37 +          (foldl add_sign (Sign.proto_pure, thys)),
   14.38          new_axioms = Symtab.null,
   14.39          parents = thys})
   14.40    end;
   14.41 @@ -496,9 +504,9 @@
   14.42  
   14.43  (*Definition of the relation =?= *)
   14.44  val flexpair_def =
   14.45 -  Thm{sign= Sign.pure, hyps= [], maxidx= 0,
   14.46 +  Thm{sign= Sign.proto_pure, hyps= [], maxidx= 0,
   14.47        prop= term_of
   14.48 -              (read_cterm Sign.pure
   14.49 +              (read_cterm Sign.proto_pure
   14.50                   ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
   14.51  
   14.52  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
    15.1 --- a/src/Pure/unify.ML	Thu Mar 02 12:07:20 1995 +0100
    15.2 +++ b/src/Pure/unify.ML	Fri Mar 03 11:48:05 1995 +0100
    15.3 @@ -53,7 +53,7 @@
    15.4  and trace_types = ref false	(*announce potential incompleteness
    15.5  				  of type unification*)
    15.6  
    15.7 -val sgr = ref(Sign.pure);
    15.8 +val sgr = ref(Sign.proto_pure);
    15.9  
   15.10  type binderlist = (string*typ) list;
   15.11