1.1 --- a/src/Pure/Proof/extraction.ML	Sat Mar 07 22:12:07 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sat Mar 07 22:16:50 2009 +0100
     1.3 @@ -37,12 +37,12 @@
     1.4    thy
     1.5    |> Theory.copy
     1.6    |> Sign.root_path
     1.7 -  |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
     1.8 +  |> Sign.add_types [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
     1.9    |> Sign.add_consts
    1.10 -      [("typeof", "'b::{} => Type", NoSyn),
    1.11 -       ("Type", "'a::{} itself => Type", NoSyn),
    1.12 -       ("Null", "Null", NoSyn),
    1.13 -       ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
    1.14 +      [(Binding.name "typeof", "'b::{} => Type", NoSyn),
    1.15 +       (Binding.name "Type", "'a::{} itself => Type", NoSyn),
    1.16 +       (Binding.name "Null", "Null", NoSyn),
    1.17 +       (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
    1.18  
    1.19  val nullT = Type ("Null", []);
    1.20  val nullt = Const ("Null", nullT);
    1.21 @@ -732,7 +732,7 @@
    1.22               val fu = Type.freeze u;
    1.23               val (def_thms, thy') = if t = nullt then ([], thy) else
    1.24                 thy
    1.25 -               |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
    1.26 +               |> Sign.add_consts_i [(Binding.name (extr_name s vs), fastype_of ft, NoSyn)]
    1.27                 |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
    1.28                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    1.29             in