src/Pure/Proof/extraction.ML
changeset 14854 61bdf2ae4dc5
parent 14472 cba7c0a3ffb3
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Jun 01 11:25:26 2004 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jun 01 12:33:50 2004 +0200
     1.3 @@ -42,12 +42,11 @@
     1.4    |> Theory.copy
     1.5    |> Theory.root_path
     1.6    |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
     1.7 -  |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")]
     1.8    |> Theory.add_consts
     1.9 -      [("typeof", "'b::logic => Type", NoSyn),
    1.10 -       ("Type", "'a::logic itself => Type", NoSyn),
    1.11 +      [("typeof", "'b::{} => Type", NoSyn),
    1.12 +       ("Type", "'a::{} itself => Type", NoSyn),
    1.13         ("Null", "Null", NoSyn),
    1.14 -       ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)];
    1.15 +       ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
    1.16  
    1.17  val nullT = Type ("Null", []);
    1.18  val nullt = Const ("Null", nullT);