removed obsolete sort 'logic';
authorwenzelm
Tue Jun 01 12:33:50 2004 +0200 (2004-06-01)
changeset 1485461bdf2ae4dc5
parent 14853 8d710bece29f
child 14855 a58abaad4f45
removed obsolete sort 'logic';
NEWS
src/CTT/CTT.thy
src/Cube/Base.thy
src/FOL/IFOL.thy
src/FOLP/IFOLP.thy
src/HOL/HOL.thy
src/HOL/Import/shuffler.ML
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Tools/record_package.ML
src/HOL/ex/Higher_Order_Logic.thy
src/Provers/splitter.ML
src/Pure/Isar/object_logic.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/term.ML
src/Pure/type_infer.ML
src/Sequents/ILL/ILL_predlog.thy
src/Sequents/LK0.thy
src/Sequents/Sequents.thy
src/ZF/Constructible/MetaExists.thy
src/ZF/QPair.thy
src/ZF/ZF.thy
     1.1 --- a/NEWS	Tue Jun 01 11:25:26 2004 +0200
     1.2 +++ b/NEWS	Tue Jun 01 12:33:50 2004 +0200
     1.3 @@ -32,6 +32,11 @@
     1.4    instead of 'nonterminals'/'syntax'.  Some very exotic syntax
     1.5    specifications may require further adaption (e.g. Cube/Base.thy).
     1.6  
     1.7 +* Pure: removed obsolete type class "logic", use the top sort {}
     1.8 +  instead.  Note that non-logical types should be declared as
     1.9 +  'nonterminals' rather than 'types'.  INCOMPATIBILITY for new
    1.10 +  object-logic specifications.
    1.11 +
    1.12  * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
    1.13  
    1.14  * Pure/Syntax: pretty pinter now supports unbreakable blocks,
     2.1 --- a/src/CTT/CTT.thy	Tue Jun 01 11:25:26 2004 +0200
     2.2 +++ b/src/CTT/CTT.thy	Tue Jun 01 12:33:50 2004 +0200
     2.3 @@ -13,9 +13,6 @@
     2.4    t
     2.5    o
     2.6  
     2.7 -arities
     2.8 -   i,t,o :: logic
     2.9 -
    2.10  consts
    2.11    (*Types*)
    2.12    F,T       :: "t"          (*F is empty, T contains one element*)
     3.1 --- a/src/Cube/Base.thy	Tue Jun 01 11:25:26 2004 +0200
     3.2 +++ b/src/Cube/Base.thy	Tue Jun 01 12:33:50 2004 +0200
     3.3 @@ -10,8 +10,6 @@
     3.4  
     3.5  types
     3.6    term
     3.7 -arities
     3.8 -  term :: logic
     3.9  
    3.10  types
    3.11    context  typing
     4.1 --- a/src/FOL/IFOL.thy	Tue Jun 01 11:25:26 2004 +0200
     4.2 +++ b/src/FOL/IFOL.thy	Tue Jun 01 12:33:50 2004 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  
     4.5  global
     4.6  
     4.7 -classes "term" < logic
     4.8 +classes "term"
     4.9  defaultsort "term"
    4.10  
    4.11  typedecl o
    4.12 @@ -264,7 +264,7 @@
    4.13  nonterminals letbinds letbind
    4.14  
    4.15  constdefs
    4.16 -  Let :: "['a::logic, 'a => 'b] => ('b::logic)"
    4.17 +  Let :: "['a::{}, 'a => 'b] => ('b::{})"
    4.18      "Let(s, f) == f(s)"
    4.19  
    4.20  syntax
     5.1 --- a/src/FOLP/IFOLP.thy	Tue Jun 01 11:25:26 2004 +0200
     5.2 +++ b/src/FOLP/IFOLP.thy	Tue Jun 01 12:33:50 2004 +0200
     5.3 @@ -10,17 +10,13 @@
     5.4  
     5.5  global
     5.6  
     5.7 -classes term < logic
     5.8 -
     5.9 +classes term
    5.10  default term
    5.11  
    5.12  types
    5.13    p
    5.14    o
    5.15  
    5.16 -arities
    5.17 -  p,o :: logic
    5.18 -
    5.19  consts  
    5.20        (*** Judgements ***)
    5.21   "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
     6.1 --- a/src/HOL/HOL.thy	Tue Jun 01 11:25:26 2004 +0200
     6.2 +++ b/src/HOL/HOL.thy	Tue Jun 01 12:33:50 2004 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  
     6.5  subsubsection {* Core syntax *}
     6.6  
     6.7 -classes type < logic
     6.8 +classes type
     6.9  defaultsort type
    6.10  
    6.11  global
     7.1 --- a/src/HOL/Import/shuffler.ML	Tue Jun 01 11:25:26 2004 +0200
     7.2 +++ b/src/HOL/Import/shuffler.ML	Tue Jun 01 12:33:50 2004 +0200
     7.3 @@ -132,8 +132,8 @@
     7.4  val def_norm =
     7.5      let
     7.6  	val cert = cterm_of (sign_of ProtoPure.thy)
     7.7 -	val aT = TFree("'a",logicS)
     7.8 -	val bT = TFree("'b",logicS)
     7.9 +	val aT = TFree("'a",[])
    7.10 +	val bT = TFree("'b",[])
    7.11  	val v = Free("v",aT)
    7.12  	val P = Free("P",aT-->bT)
    7.13  	val Q = Free("Q",aT-->bT)
    7.14 @@ -159,8 +159,8 @@
    7.15  val all_comm =
    7.16      let
    7.17  	val cert = cterm_of (sign_of ProtoPure.thy)
    7.18 -	val xT = TFree("'a",logicS)
    7.19 -	val yT = TFree("'b",logicS)
    7.20 +	val xT = TFree("'a",[])
    7.21 +	val yT = TFree("'b",[])
    7.22  	val P = Free("P",xT-->yT-->propT)
    7.23  	val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
    7.24  	val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
    7.25 @@ -404,7 +404,7 @@
    7.26      end
    7.27      handle e => (writeln "eta_expand internal error";print_exn e)
    7.28  
    7.29 -fun mk_tfree s = TFree("'"^s,logicS)
    7.30 +fun mk_tfree s = TFree("'"^s,[])
    7.31  val xT = mk_tfree "a"
    7.32  val yT = mk_tfree "b"
    7.33  val P  = Var(("P",0),xT-->yT-->propT)
    7.34 @@ -495,8 +495,6 @@
    7.35      end
    7.36      handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
    7.37  
    7.38 -fun is_logic_var sg v =
    7.39 -    Type.of_sort (Sign.tsig_of sg) (type_of v,logicS)
    7.40  
    7.41  (* Closes a theorem with respect to free and schematic variables (does
    7.42  not touch type variables, though). *)
    7.43 @@ -505,10 +503,9 @@
    7.44      let
    7.45  	val sg = sign_of_thm th
    7.46  	val c = prop_of th
    7.47 -	val all_vars = add_term_frees (c,add_term_vars(c,[]))
    7.48 -	val all_rel_vars = filter (is_logic_var sg) all_vars
    7.49 +	val vars = add_term_frees (c,add_term_vars(c,[]))
    7.50      in
    7.51 -	Drule.forall_intr_list (map (cterm_of sg) all_rel_vars) th
    7.52 +	Drule.forall_intr_list (map (cterm_of sg) vars) th
    7.53      end
    7.54      handle e => (writeln "close_thm internal error"; print_exn e)
    7.55  
    7.56 @@ -572,10 +569,9 @@
    7.57  fun set_prop thy t =
    7.58      let
    7.59  	val sg = sign_of thy
    7.60 -	val all_vars = add_term_frees (t,add_term_vars (t,[]))
    7.61 -	val all_rel_vars = filter (is_logic_var sg) all_vars
    7.62 +	val vars = add_term_frees (t,add_term_vars (t,[]))
    7.63  	val closed_t = foldr (fn (v,body) => let val vT = type_of v
    7.64 -					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (all_rel_vars,t)
    7.65 +					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
    7.66  	val rew_th = norm_term thy closed_t
    7.67  	val rhs = snd (dest_equals (cprop_of rew_th))
    7.68  
    7.69 @@ -596,7 +592,7 @@
    7.70  			val closed_th = equal_elim (symmetric rew_th) mod_th
    7.71  		    in
    7.72  			message ("Shuffler.set_prop succeeded by " ^ name);
    7.73 -			Some (name,forall_elim_list (map (cterm_of sg) all_rel_vars) closed_th)
    7.74 +			Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
    7.75  		    end
    7.76  		  | None => process thms
    7.77  	    end
     8.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jun 01 11:25:26 2004 +0200
     8.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jun 01 12:33:50 2004 +0200
     8.3 @@ -32,7 +32,7 @@
     8.4    "ALL "        :: [idts, bool] => bool                 ("'((3forall _./ _)')" [0, 10] 10)
     8.5    "EX "         :: [idts, bool] => bool                 ("'((3exists _./ _)')" [0, 10] 10)
     8.6  
     8.7 -  "_lambda"	:: [idts, 'a::logic] => 'b::logic	("(3L _./ _)" 10)
     8.8 +  "_lambda"	:: [idts, 'a] => 'b  			("(3L _./ _)" 10)
     8.9    "_applC"	:: [('b => 'a), cargs] => aprop		("(1_/ '(_'))" [1000,1000] 999)
    8.10    "_cargs" 	:: ['a, cargs] => cargs         	("_,/ _" [1000,1000] 1000)
    8.11  
     9.1 --- a/src/HOL/Tools/record_package.ML	Tue Jun 01 11:25:26 2004 +0200
     9.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jun 01 12:33:50 2004 +0200
     9.3 @@ -615,7 +615,7 @@
     9.4        val tsig = Sign.tsig_of sg
     9.5  
     9.6        fun mk_type_abbr subst name alphas = 
     9.7 -          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
     9.8 +          let val abbrT = Type (name, map (fn a => TVar ((a, 0), [])) alphas);
     9.9            in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
    9.10  
    9.11        fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
    10.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Tue Jun 01 11:25:26 2004 +0200
    10.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Tue Jun 01 12:33:50 2004 +0200
    10.3 @@ -20,7 +20,7 @@
    10.4  
    10.5  subsection {* Pure Logic *}
    10.6  
    10.7 -classes type \<subseteq> logic
    10.8 +classes type
    10.9  defaultsort type
   10.10  
   10.11  typedecl o
    11.1 --- a/src/Provers/splitter.ML	Tue Jun 01 11:25:26 2004 +0200
    11.2 +++ b/src/Provers/splitter.ML	Tue Jun 01 12:33:50 2004 +0200
    11.3 @@ -76,8 +76,8 @@
    11.4  val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
    11.5  val lift =
    11.6    let val ct = read_cterm (#sign(rep_thm Data.iffD))
    11.7 -           ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \
    11.8 -            \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
    11.9 +           ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
   11.10 +            \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
   11.11    in prove_goalw_cterm [] ct
   11.12       (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
   11.13    end;
    12.1 --- a/src/Pure/Isar/object_logic.ML	Tue Jun 01 11:25:26 2004 +0200
    12.2 +++ b/src/Pure/Isar/object_logic.ML	Tue Jun 01 12:33:50 2004 +0200
    12.3 @@ -115,7 +115,7 @@
    12.4  fun fixed_judgment sg x =
    12.5    let  (*be robust wrt. low-level errors*)
    12.6      val c = judgment_name sg;
    12.7 -    val aT = TFree ("'a", logicS);
    12.8 +    val aT = TFree ("'a", []);
    12.9      val T =
   12.10        if_none (Sign.const_type sg c) (aT --> propT)
   12.11        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
    13.1 --- a/src/Pure/Proof/extraction.ML	Tue Jun 01 11:25:26 2004 +0200
    13.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jun 01 12:33:50 2004 +0200
    13.3 @@ -42,12 +42,11 @@
    13.4    |> Theory.copy
    13.5    |> Theory.root_path
    13.6    |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
    13.7 -  |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")]
    13.8    |> Theory.add_consts
    13.9 -      [("typeof", "'b::logic => Type", NoSyn),
   13.10 -       ("Type", "'a::logic itself => Type", NoSyn),
   13.11 +      [("typeof", "'b::{} => Type", NoSyn),
   13.12 +       ("Type", "'a::{} itself => Type", NoSyn),
   13.13         ("Null", "Null", NoSyn),
   13.14 -       ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)];
   13.15 +       ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
   13.16  
   13.17  val nullT = Type ("Null", []);
   13.18  val nullt = Const ("Null", nullT);
    14.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 11:25:26 2004 +0200
    14.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Jun 01 12:33:50 2004 +0200
    14.3 @@ -34,7 +34,7 @@
    14.4  val paramT = Type ("param", []);
    14.5  val paramsT = Type ("params", []);
    14.6  val idtT = Type ("idt", []);
    14.7 -val aT = TFree ("'a", ["logic"]);
    14.8 +val aT = TFree ("'a", []);
    14.9  
   14.10  (** constants for theorems and axioms **)
   14.11  
   14.12 @@ -49,9 +49,8 @@
   14.13    sg
   14.14    |> Sign.copy
   14.15    |> Sign.add_path "/"
   14.16 -  |> Sign.add_defsort_i ["logic"]
   14.17 +  |> Sign.add_defsort_i []
   14.18    |> Sign.add_types [("proof", 0, NoSyn)]
   14.19 -  |> Sign.add_arities [("proof", [], "logic")]
   14.20    |> Sign.add_consts_i
   14.21        [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
   14.22         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    15.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Jun 01 11:25:26 2004 +0200
    15.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Jun 01 12:33:50 2004 +0200
    15.3 @@ -162,7 +162,7 @@
    15.4        | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
    15.5            let
    15.6              val (env', T) = (case opT of
    15.7 -              None => mk_tvar (env, logicS) | Some T => (env, T));
    15.8 +              None => mk_tvar (env, []) | Some T => (env, T));
    15.9              val (t, prf, cnstrts, env'', vTs') =
   15.10                mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
   15.11            in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, Some T, prf),
   15.12 @@ -216,7 +216,7 @@
   15.13                 end
   15.14             | (u, prf, cnstrts, env', vTs') =>
   15.15                 let
   15.16 -                 val (env1, T) = mk_tvar (env', ["logic"]);
   15.17 +                 val (env1, T) = mk_tvar (env', []);
   15.18                   val (env2, v) = mk_var env1 Ts (T --> propT);
   15.19                   val (env3, t) = mk_var env2 Ts T
   15.20                 in
    16.1 --- a/src/Pure/axclass.ML	Tue Jun 01 11:25:26 2004 +0200
    16.2 +++ b/src/Pure/axclass.ML	Tue Jun 01 12:33:50 2004 +0200
    16.3 @@ -214,9 +214,6 @@
    16.4  
    16.5  (* errors *)
    16.6  
    16.7 -fun err_not_logic c =
    16.8 -  error ("Axiomatic class " ^ quote c ^ " not subclass of " ^ quote logicC);
    16.9 -
   16.10  fun err_bad_axsort ax c =
   16.11    error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
   16.12  
   16.13 @@ -243,19 +240,16 @@
   16.14      (*prepare abstract axioms*)
   16.15      fun abs_axm ax =
   16.16        if null (term_tfrees ax) then
   16.17 -        Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax)
   16.18 +        Logic.mk_implies (Logic.mk_inclass (aT [], class), ax)
   16.19        else map_term_tfrees (K (aT [class])) ax;
   16.20      val abs_axms = map (abs_axm o #2) axms;
   16.21  
   16.22 -    (*prepare introduction rule*)
   16.23 -    val _ = if Sign.subsort class_sign ([class], logicS) then () else err_not_logic class;
   16.24 -
   16.25      fun axm_sort (name, ax) =
   16.26        (case term_tfrees ax of
   16.27          [] => []
   16.28        | [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
   16.29        | _ => err_bad_tfrees name);
   16.30 -    val axS = Sign.certify_sort class_sign (logicC :: flat (map axm_sort axms));
   16.31 +    val axS = Sign.certify_sort class_sign (flat (map axm_sort axms));
   16.32  
   16.33      val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
   16.34      fun inclass c = Logic.mk_inclass (aT axS, c);
    17.1 --- a/src/Pure/drule.ML	Tue Jun 01 11:25:26 2004 +0200
    17.2 +++ b/src/Pure/drule.ML	Tue Jun 01 12:33:50 2004 +0200
    17.3 @@ -548,16 +548,16 @@
    17.4  fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
    17.5  
    17.6  val reflexive_thm =
    17.7 -  let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
    17.8 +  let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),[])))
    17.9    in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
   17.10  
   17.11  val symmetric_thm =
   17.12 -  let val xy = read_prop "x::'a::logic == y"
   17.13 +  let val xy = read_prop "x == y"
   17.14    in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
   17.15  
   17.16  val transitive_thm =
   17.17 -  let val xy = read_prop "x::'a::logic == y"
   17.18 -      val yz = read_prop "y::'a::logic == z"
   17.19 +  let val xy = read_prop "x == y"
   17.20 +      val yz = read_prop "y == z"
   17.21        val xythm = Thm.assume xy and yzthm = Thm.assume yz
   17.22    in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   17.23  
   17.24 @@ -698,7 +698,7 @@
   17.25  val norm_hhf_eq =
   17.26    let
   17.27      val cert = Thm.cterm_of proto_sign;
   17.28 -    val aT = TFree ("'a", Term.logicS);
   17.29 +    val aT = TFree ("'a", []);
   17.30      val all = Term.all aT;
   17.31      val x = Free ("x", aT);
   17.32      val phi = Free ("phi", propT);
    18.1 --- a/src/Pure/proofterm.ML	Tue Jun 01 11:25:26 2004 +0200
    18.2 +++ b/src/Pure/proofterm.ML	Tue Jun 01 12:33:50 2004 +0200
    18.3 @@ -685,8 +685,8 @@
    18.4  
    18.5  (***** axioms for equality *****)
    18.6  
    18.7 -val aT = TFree ("'a", ["logic"]);
    18.8 -val bT = TFree ("'b", ["logic"]);
    18.9 +val aT = TFree ("'a", []);
   18.10 +val bT = TFree ("'b", []);
   18.11  val x = Free ("x", aT);
   18.12  val y = Free ("y", aT);
   18.13  val z = Free ("z", aT);
    19.1 --- a/src/Pure/pure_thy.ML	Tue Jun 01 11:25:26 2004 +0200
    19.2 +++ b/src/Pure/pure_thy.ML	Tue Jun 01 12:33:50 2004 +0200
    19.3 @@ -500,17 +500,7 @@
    19.4      fun type_of (raw_name, vs, mx) =
    19.5        if null (duplicates vs) then (raw_name, length vs, mx)
    19.6        else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
    19.7 -
    19.8 -    fun arity_of (raw_name, len, mx) =
    19.9 -      (full (Syntax.type_name raw_name mx), replicate len logicS, logicS);
   19.10 -
   19.11 -    val types = map type_of decls;
   19.12 -    val arities = map arity_of types;
   19.13 -  in
   19.14 -    thy
   19.15 -    |> Theory.add_types types
   19.16 -    |> Theory.add_arities_i arities
   19.17 -  end;
   19.18 +  in thy |> Theory.add_types (map type_of decls) end;
   19.19  
   19.20  
   19.21  
   19.22 @@ -531,12 +521,6 @@
   19.23      ("prop", 0, NoSyn),
   19.24      ("itself", 1, NoSyn),
   19.25      ("dummy", 0, NoSyn)]
   19.26 -  |> Theory.add_classes_i [(logicC, [])]
   19.27 -  |> Theory.add_defsort_i logicS
   19.28 -  |> Theory.add_arities_i
   19.29 -   [("fun", [logicS, logicS], logicS),
   19.30 -    ("prop", [], logicS),
   19.31 -    ("itself", [logicS], logicS)]
   19.32    |> Theory.add_nonterminals Syntax.pure_nonterms
   19.33    |> Theory.add_syntax Syntax.pure_syntax
   19.34    |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   19.35 @@ -544,17 +528,17 @@
   19.36     [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
   19.37      (Term.dummy_patternN, "aprop", Delimfix "'_")]
   19.38    |> Theory.add_consts
   19.39 -   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   19.40 +   [("==", "['a, 'a] => prop", InfixrName ("==", 2)),
   19.41      ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   19.42      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   19.43      ("Goal", "prop => prop", NoSyn),
   19.44      ("TYPE", "'a itself", NoSyn),
   19.45      (Term.dummy_patternN, "'a", Delimfix "'_")]
   19.46    |> Theory.add_finals_i false
   19.47 -    [Const("==",[TFree("'a",[]),TFree("'a",[])]--->propT),
   19.48 -     Const("==>",[propT,propT]--->propT),
   19.49 -     Const("all",(TFree("'a",logicS)-->propT)-->propT),
   19.50 -     Const("TYPE",a_itselfT)]
   19.51 +    [Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT),
   19.52 +     Const("==>", [propT, propT] ---> propT),
   19.53 +     Const("all", (TFree("'a", []) --> propT) --> propT),
   19.54 +     Const("TYPE", a_itselfT)]
   19.55    |> Theory.add_modesyntax ("", false)
   19.56      (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   19.57    |> Theory.add_trfuns Syntax.pure_trfuns
    20.1 --- a/src/Pure/term.ML	Tue Jun 01 11:25:26 2004 +0200
    20.2 +++ b/src/Pure/term.ML	Tue Jun 01 12:33:50 2004 +0200
    20.3 @@ -76,8 +76,6 @@
    20.4    val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
    20.5    val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
    20.6    val dummyT: typ
    20.7 -  val logicC: class
    20.8 -  val logicS: sort
    20.9    val itselfT: typ -> typ
   20.10    val a_itselfT: typ
   20.11    val propT: typ
   20.12 @@ -415,11 +413,8 @@
   20.13  
   20.14  (** Connectives of higher order logic **)
   20.15  
   20.16 -val logicC: class = "logic";
   20.17 -val logicS: sort = [logicC];
   20.18 -
   20.19  fun itselfT ty = Type ("itself", [ty]);
   20.20 -val a_itselfT = itselfT (TFree ("'a", logicS));
   20.21 +val a_itselfT = itselfT (TFree ("'a", []));
   20.22  
   20.23  val propT : typ = Type("prop",[]);
   20.24  
    21.1 --- a/src/Pure/type_infer.ML	Tue Jun 01 11:25:26 2004 +0200
    21.2 +++ b/src/Pure/type_infer.ML	Tue Jun 01 12:33:50 2004 +0200
    21.3 @@ -103,7 +103,7 @@
    21.4  (* pretyp(s)_of *)
    21.5  
    21.6  fun anyT S = TFree ("'_dummy_", S);
    21.7 -val logicT = anyT logicS;
    21.8 +val logicT = anyT [];
    21.9  
   21.10  (*indicate polymorphic Vars*)
   21.11  fun polymorphicT T = Type ("_polymorphic_", [T]);
    22.1 --- a/src/Sequents/ILL/ILL_predlog.thy	Tue Jun 01 11:25:26 2004 +0200
    22.2 +++ b/src/Sequents/ILL/ILL_predlog.thy	Tue Jun 01 12:33:50 2004 +0200
    22.3 @@ -7,13 +7,8 @@
    22.4  ILL_predlog  =  ILL +
    22.5  
    22.6  types
    22.7 -
    22.8      plf
    22.9      
   22.10 -arities
   22.11 -
   22.12 -    plf :: logic
   22.13 -    
   22.14  consts
   22.15  
   22.16    "&"   :: "[plf,plf] => plf"   (infixr 35)
    23.1 --- a/src/Sequents/LK0.thy	Tue Jun 01 11:25:26 2004 +0200
    23.2 +++ b/src/Sequents/LK0.thy	Tue Jun 01 12:33:50 2004 +0200
    23.3 @@ -13,11 +13,8 @@
    23.4  
    23.5  global
    23.6  
    23.7 -classes
    23.8 -  term < logic
    23.9 -
   23.10 -default
   23.11 -  term
   23.12 +classes term
   23.13 +default term
   23.14  
   23.15  consts
   23.16  
    24.1 --- a/src/Sequents/Sequents.thy	Tue Jun 01 11:25:26 2004 +0200
    24.2 +++ b/src/Sequents/Sequents.thy	Tue Jun 01 12:33:50 2004 +0200
    24.3 @@ -14,9 +14,6 @@
    24.4  types
    24.5    o 
    24.6  
    24.7 -arities
    24.8 -  o :: logic
    24.9 -
   24.10  
   24.11  (* Sequences *)
   24.12  
    25.1 --- a/src/ZF/Constructible/MetaExists.thy	Tue Jun 01 11:25:26 2004 +0200
    25.2 +++ b/src/ZF/Constructible/MetaExists.thy	Tue Jun 01 12:33:50 2004 +0200
    25.3 @@ -11,7 +11,7 @@
    25.4  quantify over classes.  Yields a proposition rather than a FOL formula.*}
    25.5  
    25.6  constdefs
    25.7 -  ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
    25.8 +  ex :: "(('a::{}) => prop) => prop"            (binder "?? " 0)
    25.9    "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
   25.10  
   25.11  syntax (xsymbols)
    26.1 --- a/src/ZF/QPair.thy	Tue Jun 01 11:25:26 2004 +0200
    26.2 +++ b/src/ZF/QPair.thy	Tue Jun 01 12:33:50 2004 +0200
    26.3 @@ -31,7 +31,7 @@
    26.4    qsnd :: "i => i"
    26.5      "qsnd(p) == THE b. EX a. p=<a;b>"
    26.6  
    26.7 -  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
    26.8 +  qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)
    26.9      "qsplit(c,p) == c(qfst(p), qsnd(p))"
   26.10  
   26.11    qconverse :: "i => i"
    27.1 --- a/src/ZF/ZF.thy	Tue Jun 01 11:25:26 2004 +0200
    27.2 +++ b/src/ZF/ZF.thy	Tue Jun 01 12:33:50 2004 +0200
    27.3 @@ -61,7 +61,7 @@
    27.4    Pair  :: "[i, i] => i"
    27.5    fst   :: "i => i"
    27.6    snd   :: "i => i"
    27.7 -  split :: "[[i, i] => 'a, i] => 'a::logic"  --{*for pattern-matching*}
    27.8 +  split :: "[[i, i] => 'a, i] => 'a::{}"  --{*for pattern-matching*}
    27.9  
   27.10  text {*Sigma and Pi Operators *}
   27.11  consts