src/Pure/pure_thy.ML
changeset 16441 92a8a25e53c5
parent 16336 e3892698c57d
child 16493 d0f6c33b2300
     1.1 --- a/src/Pure/pure_thy.ML	Fri Jun 17 18:33:25 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Jun 17 18:33:26 2005 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Theorem database, derived theory operations, and the ProtoPure theory.
     1.8 +Theorem storage.  The ProtoPure theory.
     1.9  *)
    1.10  
    1.11  signature BASIC_PURE_THY =
    1.12 @@ -25,12 +25,12 @@
    1.13    include BASIC_PURE_THY
    1.14    datatype interval = FromTo of int * int | From of int | Single of int
    1.15    val string_of_thmref: thmref -> string
    1.16 +  val theorem_space: theory -> NameSpace.T
    1.17    val get_thm_closure: theory -> thmref -> thm
    1.18    val get_thms_closure: theory -> thmref -> thm list
    1.19    val single_thm: string -> thm list -> thm
    1.20    val select_thm: thmref -> thm list -> thm list
    1.21    val selections: string * thm list -> (thmref * thm) list
    1.22 -  val extern_thm_sg: Sign.sg -> string -> xstring
    1.23    val fact_index_of: theory -> FactIndex.T
    1.24    val valid_thms: theory -> thmref * thm list -> bool
    1.25    val thms_containing: theory -> FactIndex.spec -> (string * thm list) list
    1.26 @@ -47,31 +47,27 @@
    1.27    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
    1.28      -> theory * thm list list
    1.29    val note_thmss: theory attribute -> ((bstring * theory attribute list) *
    1.30 -    (thmref * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
    1.31 +    (thmref * theory attribute list) list) list ->
    1.32 +    theory -> theory * (bstring * thm list) list
    1.33    val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
    1.34 -    (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
    1.35 -  val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
    1.36 -  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    1.37 -  val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory
    1.38 -    -> theory * thm list list
    1.39 -  val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory
    1.40 -    -> theory * thm list list
    1.41 -  val add_defs: bool -> ((bstring * string) * theory attribute list) list
    1.42 -    -> theory -> theory * thm list
    1.43 -  val add_defs_i: bool -> ((bstring * term) * theory attribute list) list
    1.44 -    -> theory -> theory * thm list
    1.45 -  val add_defss: bool -> ((bstring * string list) * theory attribute list) list
    1.46 -    -> theory -> theory * thm list list
    1.47 -  val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list
    1.48 -    -> theory -> theory * thm list list
    1.49 -  val get_name: theory -> string
    1.50 -  val put_name: string -> theory -> theory
    1.51 -  val global_path: theory -> theory
    1.52 -  val local_path: theory -> theory
    1.53 -  val begin_theory: string -> theory list -> theory
    1.54 -  val end_theory: theory -> theory
    1.55 -  val checkpoint: theory -> theory
    1.56 -  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    1.57 +    (thm list * theory attribute list) list) list ->
    1.58 +    theory -> theory * (bstring * thm list) list
    1.59 +  val add_axioms: ((bstring * string) * theory attribute list) list ->
    1.60 +    theory -> theory * thm list
    1.61 +  val add_axioms_i: ((bstring * term) * theory attribute list) list ->
    1.62 +    theory -> theory * thm list
    1.63 +  val add_axiomss: ((bstring * string list) * theory attribute list) list ->
    1.64 +    theory -> theory * thm list list
    1.65 +  val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
    1.66 +    theory -> theory * thm list list
    1.67 +  val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
    1.68 +    theory -> theory * thm list
    1.69 +  val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
    1.70 +    theory -> theory * thm list
    1.71 +  val add_defss: bool -> ((bstring * string list) * theory attribute list) list ->
    1.72 +    theory -> theory * thm list list
    1.73 +  val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
    1.74 +    theory -> theory * thm list list
    1.75  end;
    1.76  
    1.77  structure PureThy: PURE_THY =
    1.78 @@ -80,53 +76,46 @@
    1.79  
    1.80  (*** theorem database ***)
    1.81  
    1.82 -(** data kind 'Pure/theorems' **)
    1.83 +(** dataype theorems **)
    1.84  
    1.85 -structure TheoremsDataArgs =
    1.86 -struct
    1.87 +fun pretty_theorems thy theorems =
    1.88 +  let
    1.89 +    val prt_thm = Display.pretty_thm_sg thy;
    1.90 +    fun prt_thms (name, [th]) =
    1.91 +          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
    1.92 +      | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    1.93 +    val thmss = NameSpace.extern_table theorems;
    1.94 +  in Pretty.big_list "theorems:" (map prt_thms thmss) end;
    1.95 +
    1.96 +structure TheoremsData = TheoryDataFun
    1.97 +(struct
    1.98    val name = "Pure/theorems";
    1.99 -
   1.100    type T =
   1.101 -    {theorems: thm list NameSpace.table,
   1.102 -      index: FactIndex.T} ref;
   1.103 +   {theorems: thm list NameSpace.table,
   1.104 +    index: FactIndex.T} ref;
   1.105  
   1.106    fun mk_empty _ =
   1.107      ref {theorems = NameSpace.empty_table, index = FactIndex.empty}: T;
   1.108  
   1.109    val empty = mk_empty ();
   1.110    fun copy (ref x) = ref x;
   1.111 -  val prep_ext = mk_empty;
   1.112 -  val merge = mk_empty;
   1.113 -
   1.114 -  fun pretty sg (ref {theorems, index = _}) =
   1.115 -    let
   1.116 -      val prt_thm = Display.pretty_thm_sg sg;
   1.117 -      fun prt_thms (name, [th]) =
   1.118 -            Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
   1.119 -        | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
   1.120 +  val extend = mk_empty;
   1.121 +  fun merge _ = mk_empty;
   1.122 +  fun print thy (ref {theorems, index}) = Pretty.writeln (pretty_theorems thy theorems);
   1.123 +end);
   1.124  
   1.125 -      val thmss = NameSpace.extern_table theorems;
   1.126 -    in Pretty.big_list "theorems:" (map prt_thms thmss) end;
   1.127 -
   1.128 -  fun print sg data = Pretty.writeln (pretty sg data);
   1.129 -end;
   1.130 -
   1.131 -structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
   1.132 -val get_theorems_sg = TheoremsData.get_sg;
   1.133  val get_theorems = TheoremsData.get;
   1.134 -
   1.135 -val extern_thm_sg = NameSpace.extern o #1 o #theorems o ! o get_theorems_sg;
   1.136 +val theorem_space = #1 o #theorems o ! o get_theorems;
   1.137  val fact_index_of = #index o ! o get_theorems;
   1.138  
   1.139  
   1.140 -
   1.141  (* print theory *)
   1.142  
   1.143  val print_theorems = TheoremsData.print;
   1.144  
   1.145  fun print_theory thy =
   1.146    Display.pretty_full_theory thy @
   1.147 -  [TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)]
   1.148 +    [pretty_theorems thy (#theorems (! (get_theorems thy)))]
   1.149    |> Pretty.chunks |> Pretty.writeln;
   1.150  
   1.151  
   1.152 @@ -192,33 +181,32 @@
   1.153  
   1.154  fun lookup_thms thy =
   1.155    let
   1.156 -    val sg_ref = Sign.self_ref (Theory.sign_of thy);
   1.157 +    val thy_ref = Theory.self_ref thy;
   1.158      val ref {theorems = (space, thms), ...} = get_theorems thy;
   1.159    in
   1.160      fn name =>
   1.161 -      Option.map (map (Thm.transfer_sg (Sign.deref sg_ref)))        (*semi-dynamic identity*)
   1.162 -      (Symtab.lookup (thms, NameSpace.intern space name))           (*static content*)
   1.163 +      Option.map (map (Thm.transfer (Theory.deref thy_ref)))    (*dynamic identity*)
   1.164 +      (Symtab.lookup (thms, NameSpace.intern space name))       (*static content*)
   1.165    end;
   1.166  
   1.167  fun get_thms_closure thy =
   1.168 -  let val closures = map lookup_thms (thy :: Theory.ancestors_of thy)
   1.169 -  in fn namei as (name, _) => select_thm namei
   1.170 -    (the_thms name (get_first (fn f => f name) closures))
   1.171 +  let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in
   1.172 +    fn (name, i) => select_thm (name, i) (the_thms name (get_first (fn f => f name) closures))
   1.173    end;
   1.174  
   1.175  fun get_thm_closure thy =
   1.176    let val get = get_thms_closure thy
   1.177 -  in fn namei as (name, _) => single_thm name (get namei) end;
   1.178 +  in fn (name, i) => single_thm name (get (name, i)) end;
   1.179  
   1.180  
   1.181 -(* get_thm etc. *)
   1.182 +(* get_thms etc. *)
   1.183  
   1.184 -fun get_thms theory (namei as (name, _)) =
   1.185 +fun get_thms theory (name, i) =
   1.186    get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
   1.187 -  |> the_thms name |> select_thm namei |> map (Thm.transfer theory);
   1.188 +  |> the_thms name |> select_thm (name, i) |> map (Thm.transfer theory);
   1.189  
   1.190  fun get_thmss thy names = List.concat (map (get_thms thy) names);
   1.191 -fun get_thm thy (namei as (name, _)) = single_thm name (get_thms thy namei);
   1.192 +fun get_thm thy (name, i) = single_thm name (get_thms thy (name, i));
   1.193  
   1.194  
   1.195  (* thms_containing etc. *)
   1.196 @@ -254,7 +242,7 @@
   1.197  
   1.198  (** store theorems **)                    (*DESTRUCTIVE*)
   1.199  
   1.200 -(* hiding -- affects current theory node only! *)
   1.201 +(* hiding -- affects current theory node only *)
   1.202  
   1.203  fun hide_thms fully names thy =
   1.204    let
   1.205 @@ -266,20 +254,21 @@
   1.206  (* naming *)
   1.207  
   1.208  fun gen_names j len name =
   1.209 -  map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len);
   1.210 +  map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len);
   1.211  
   1.212  fun name_multi name xs = gen_names 0 (length xs) name ~~ xs;
   1.213  
   1.214 -fun name_thm pre (p as (_, thm)) =
   1.215 -  if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm p;
   1.216 +fun name_thm pre (name, thm) =
   1.217 +  if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm (name, thm);
   1.218  
   1.219  fun name_thms pre name [x] = [name_thm pre (name, x)]
   1.220    | name_thms pre name xs = map (name_thm pre) (name_multi name xs);
   1.221  
   1.222 -fun name_thmss name xs = (case filter_out (null o fst) xs of
   1.223 +fun name_thmss name xs =
   1.224 +  (case filter_out (null o fst) xs of
   1.225      [([x], z)] => [([name_thm true (name, x)], z)]
   1.226 -  | _ => snd (foldl_map (fn (i, (ys, z)) => (i + length ys,
   1.227 -  (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
   1.228 +  | _ => snd (foldl_map (fn (i, (ys, z)) =>
   1.229 +    (i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
   1.230  
   1.231  
   1.232  (* enter_thms *)
   1.233 @@ -287,33 +276,31 @@
   1.234  fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
   1.235  fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
   1.236  
   1.237 -fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms)
   1.238 -  | enter_thms sg pre_name post_name app_att thy (bname, thms) =
   1.239 +fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms)
   1.240 +  | enter_thms pre_name post_name app_att (bname, thms) thy =
   1.241        let
   1.242 -        val name = Sign.full_name sg bname;
   1.243 -        val (thy', thms') = app_att (thy, pre_name name thms);
   1.244 -        val named_thms = post_name name thms';
   1.245 -
   1.246 -        val r as ref {theorems = (space, theorems), index} = get_theorems_sg sg;
   1.247 -        val space' = Sign.declare_name sg name space;
   1.248 -        val theorems' = Symtab.update ((name, named_thms), theorems);
   1.249 -        val index' = FactIndex.add (K false) (name, named_thms) index;
   1.250 +        val name = Sign.full_name thy bname;
   1.251 +        val r as ref {theorems = (space, theorems), index} = get_theorems thy;
   1.252 +        val space' = Sign.declare_name thy name space;
   1.253 +        val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
   1.254 +        val theorems' = Symtab.update ((name, thms'), theorems);
   1.255 +        val index' = FactIndex.add (K false) (name, thms') index;
   1.256        in
   1.257          (case Symtab.lookup (theorems, name) of
   1.258            NONE => ()
   1.259 -        | SOME thms' =>
   1.260 -            if Thm.eq_thms (thms', named_thms) then warn_same name
   1.261 +        | SOME thms'' =>
   1.262 +            if Thm.eq_thms (thms', thms'') then warn_same name
   1.263              else warn_overwrite name);
   1.264          r := {theorems = (space', theorems'), index = index'};
   1.265 -        (thy', named_thms)
   1.266 +        (thy', thms')
   1.267        end;
   1.268  
   1.269  
   1.270  (* add_thms(s) *)
   1.271  
   1.272 -fun add_thms_atts pre_name ((bname, thms), atts) thy =
   1.273 -  enter_thms (Theory.sign_of thy) pre_name (name_thms false)
   1.274 -    (Thm.applys_attributes o rpair atts) thy (bname, thms);
   1.275 +fun add_thms_atts pre_name ((bname, thms), atts) =
   1.276 +  enter_thms pre_name (name_thms false)
   1.277 +    (Thm.applys_attributes o rpair atts) (bname, thms);
   1.278  
   1.279  fun gen_add_thmss pre_name args theory =
   1.280    foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args);
   1.281 @@ -332,8 +319,8 @@
   1.282  fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
   1.283    let
   1.284      fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
   1.285 -    val (thy', thms) = enter_thms (Theory.sign_of thy)
   1.286 -      name_thmss (name_thms false) (apsnd List.concat o foldl_map app) thy
   1.287 +    val (thy', thms) = thy |> enter_thms
   1.288 +      name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
   1.289        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
   1.290    in (thy', (bname, thms)) end;
   1.291  
   1.292 @@ -355,42 +342,44 @@
   1.293    in (thy', th') end;
   1.294  
   1.295  
   1.296 -(* smart_store_thms *)
   1.297 +(* smart_store_thms(_open) *)
   1.298  
   1.299 -fun gen_smart_store_thms _ (name, []) =
   1.300 +local
   1.301 +
   1.302 +fun smart_store _ (name, []) =
   1.303        error ("Cannot store empty list of theorems: " ^ quote name)
   1.304 -  | gen_smart_store_thms name_thm (name, [thm]) =
   1.305 -      snd (enter_thms (Thm.sign_of_thm thm) (name_thm true) (name_thm false)
   1.306 -        I () (name, [thm]))
   1.307 -  | gen_smart_store_thms name_thm (name, thms) =
   1.308 +  | smart_store name_thm (name, [thm]) =
   1.309 +      #2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
   1.310 +  | smart_store name_thm (name, thms) =
   1.311        let
   1.312 -        val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
   1.313 -        val sg_ref = Library.foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
   1.314 -      in snd (enter_thms (Sign.deref sg_ref) (name_thm true) (name_thm false)
   1.315 -        I () (name, thms))
   1.316 -      end;
   1.317 +        fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
   1.318 +        val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
   1.319 +      in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
   1.320  
   1.321 -val smart_store_thms = gen_smart_store_thms name_thms;
   1.322 -val smart_store_thms_open = gen_smart_store_thms (K (K I));
   1.323 +in
   1.324 +
   1.325 +val smart_store_thms = smart_store name_thms;
   1.326 +val smart_store_thms_open = smart_store (K (K I));
   1.327 +
   1.328 +end;
   1.329  
   1.330  
   1.331  (* forall_elim_vars (belongs to drule.ML) *)
   1.332  
   1.333  (*Replace outermost quantified variable by Var of given index.*)
   1.334  fun forall_elim_var i th =
   1.335 -    let val {prop,sign,...} = rep_thm th
   1.336 -    in case prop of
   1.337 +  let val {prop, thy, ...} = Thm.rep_thm th
   1.338 +  in case prop of
   1.339          Const ("all", _) $ Abs (a, T, _) =>
   1.340            let val used = map (fst o fst)
   1.341              (List.filter (equal i o snd o fst) (Term.add_vars ([], prop)))
   1.342 -          in forall_elim (cterm_of sign (Var ((variant used a, i), T))) th end
   1.343 -      | _ => raise THM ("forall_elim_var", i, [th])
   1.344 -    end;
   1.345 +          in Thm.forall_elim (Thm.cterm_of thy (Var ((variant used a, i), T))) th end
   1.346 +     | _ => raise THM ("forall_elim_var", i, [th])
   1.347 +  end;
   1.348  
   1.349  (*Repeat forall_elim_var until all outer quantifiers are removed*)
   1.350  fun forall_elim_vars i th =
   1.351 -    forall_elim_vars i (forall_elim_var i th)
   1.352 -        handle THM _ => th;
   1.353 +  forall_elim_vars i (forall_elim_var i th) handle THM _ => th;
   1.354  
   1.355  
   1.356  (* store axioms as theorems *)
   1.357 @@ -428,86 +417,17 @@
   1.358  
   1.359  
   1.360  
   1.361 -(*** derived theory operations ***)
   1.362 -
   1.363 -(** theory management **)
   1.364 -
   1.365 -(* data kind 'Pure/theory_management' *)
   1.366 -
   1.367 -structure TheoryManagementDataArgs =
   1.368 -struct
   1.369 -  val name = "Pure/theory_management";
   1.370 -  type T = {name: string, version: int};
   1.371 -
   1.372 -  val empty = {name = "", version = 0};
   1.373 -  val copy = I;
   1.374 -  val prep_ext  = I;
   1.375 -  fun merge _ = empty;
   1.376 -  fun print _ _ = ();
   1.377 -end;
   1.378 -
   1.379 -structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs);
   1.380 -val get_info = TheoryManagementData.get;
   1.381 -val put_info = TheoryManagementData.put;
   1.382 -
   1.383 -
   1.384 -(* get / put name *)
   1.385 -
   1.386 -val get_name = #name o get_info;
   1.387 -fun put_name name = put_info {name = name, version = 0};
   1.388 -
   1.389 -
   1.390 -(* control prefixing of theory name *)
   1.391 -
   1.392 -val global_path = Theory.root_path;
   1.393 -
   1.394 -fun local_path thy =
   1.395 -  thy |> Theory.root_path |> Theory.add_path (get_name thy);
   1.396 -
   1.397 -
   1.398 -(* begin / end theory *)
   1.399 -
   1.400 -fun begin_theory name thys =
   1.401 -  Theory.prep_ext_merge thys
   1.402 -  |> put_name name
   1.403 -  |> local_path;
   1.404 -
   1.405 -fun end_theory thy =
   1.406 -  thy
   1.407 -  |> Theory.add_name (get_name thy);
   1.408 -
   1.409 -fun checkpoint thy =
   1.410 -  if is_draft thy then
   1.411 -    let val {name, version} = get_info thy in
   1.412 -      thy
   1.413 -      |> Theory.add_name (name ^ ":" ^ string_of_int version)
   1.414 -      |> put_info {name = name, version = version + 1}
   1.415 -    end
   1.416 -  else thy;
   1.417 -
   1.418 -
   1.419 -
   1.420 -(** add logical types **)
   1.421 -
   1.422 -fun add_typedecls decls thy =
   1.423 -  let
   1.424 -    val full = Sign.full_name (Theory.sign_of thy);
   1.425 -
   1.426 -    fun type_of (raw_name, vs, mx) =
   1.427 -      if null (duplicates vs) then (raw_name, length vs, mx)
   1.428 -      else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
   1.429 -  in thy |> Theory.add_types (map type_of decls) end;
   1.430 -
   1.431 -
   1.432 -
   1.433  (*** the ProtoPure theory ***)
   1.434  
   1.435 +val aT = TFree ("'a", []);
   1.436 +val A = Free ("A", propT);
   1.437 +
   1.438  val proto_pure =
   1.439 -  Theory.pre_pure
   1.440 -  |> TheoryManagementData.init |> put_name "ProtoPure"
   1.441 +  Context.pre_pure
   1.442 +  |> Sign.init
   1.443 +  |> Theory.init
   1.444 +  |> Proofterm.init
   1.445    |> TheoremsData.init
   1.446 -  |> Proofterm.init
   1.447 -  |> global_path
   1.448    |> Theory.add_types
   1.449     [("fun", 2, NoSyn),
   1.450      ("prop", 0, NoSyn),
   1.451 @@ -518,30 +438,30 @@
   1.452    |> Theory.add_syntax Syntax.pure_appl_syntax
   1.453    |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   1.454    |> Theory.add_syntax
   1.455 -   [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
   1.456 +   [("==>", "prop => prop => prop", Delimfix "op ==>"),
   1.457      (Term.dummy_patternN, "aprop", Delimfix "'_")]
   1.458    |> Theory.add_consts
   1.459 -   [("==", "['a, 'a] => prop", InfixrName ("==", 2)),
   1.460 -    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   1.461 +   [("==", "'a => 'a => prop", InfixrName ("==", 2)),
   1.462 +    ("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   1.463      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   1.464      ("Goal", "prop => prop", NoSyn),
   1.465      ("TYPE", "'a itself", NoSyn),
   1.466      (Term.dummy_patternN, "'a", Delimfix "'_")]
   1.467    |> Theory.add_finals_i false
   1.468 -    [Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT),
   1.469 -     Const("==>", [propT, propT] ---> propT),
   1.470 -     Const("all", (TFree("'a", []) --> propT) --> propT),
   1.471 -     Const("TYPE", a_itselfT)]
   1.472 +    [Const ("==", [aT, aT] ---> propT),
   1.473 +     Const ("==>", [propT, propT] ---> propT),
   1.474 +     Const ("all", (aT --> propT) --> propT),
   1.475 +     Const ("TYPE", a_itselfT)]
   1.476    |> Theory.add_modesyntax ("", false)
   1.477      (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   1.478    |> Theory.add_trfuns Syntax.pure_trfuns
   1.479    |> Theory.add_trfunsT Syntax.pure_trfunsT
   1.480 -  |> local_path
   1.481 +  |> Sign.local_path
   1.482    |> (#1 oo (add_defs_i false o map Thm.no_attributes))
   1.483 -   [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
   1.484 +   [("Goal_def", Logic.mk_equals (Logic.mk_goal A, A))]
   1.485    |> (#1 o add_thmss [(("nothing", []), [])])
   1.486    |> Theory.add_axioms_i Proofterm.equality_axms
   1.487 -  |> end_theory;
   1.488 +  |> Context.end_theory;
   1.489  
   1.490  structure ProtoPure =
   1.491  struct