src/Pure/Proof/extraction.ML

--- a/src/Pure/Proof/extraction.ML	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Jun 01 12:33:50 2004 +0200
@@ -42,12 +42,11 @@
   |> Theory.copy
   |> Theory.root_path
   |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
-  |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")]
   |> Theory.add_consts
-      [("typeof", "'b::logic => Type", NoSyn),
-       ("Type", "'a::logic itself => Type", NoSyn),
+      [("typeof", "'b::{} => Type", NoSyn),
+       ("Type", "'a::{} itself => Type", NoSyn),
        ("Null", "Null", NoSyn),
-       ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)];
+       ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
 
 val nullT = Type ("Null", []);
 val nullt = Const ("Null", nullT);