src/Pure/Proof/extraction.ML
changeset 56436 30ccec1e82fb
parent 56239 17df7145a871
child 58436 fe9de4089345
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Apr 06 15:38:54 2014 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Apr 06 15:43:45 2014 +0200
     1.3 @@ -36,12 +36,14 @@
     1.4  
     1.5  val add_syntax =
     1.6    Sign.root_path
     1.7 -  #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
     1.8 +  #> Sign.add_types_global
     1.9 +    [(Binding.make ("Type", @{here}), 0, NoSyn),
    1.10 +     (Binding.make ("Null", @{here}), 0, NoSyn)]
    1.11    #> Sign.add_consts
    1.12 -      [(Binding.name "typeof", typ "'b => Type", NoSyn),
    1.13 -       (Binding.name "Type", typ "'a itself => Type", NoSyn),
    1.14 -       (Binding.name "Null", typ "Null", NoSyn),
    1.15 -       (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)];
    1.16 +    [(Binding.make ("typeof", @{here}), typ "'b => Type", NoSyn),
    1.17 +     (Binding.make ("Type", @{here}), typ "'a itself => Type", NoSyn),
    1.18 +     (Binding.make ("Null", @{here}), typ "Null", NoSyn),
    1.19 +     (Binding.make ("realizes", @{here}), typ "'a => 'b => 'b", NoSyn)];
    1.20  
    1.21  val nullT = Type ("Null", []);
    1.22  val nullt = Const ("Null", nullT);