src/Pure/Proof/extraction.ML
changeset 56239 17df7145a871
parent 56206 7adec2a527f5
child 56436 30ccec1e82fb
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 21 08:13:23 2014 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 21 10:45:03 2014 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  val add_syntax =
     1.5    Sign.root_path
     1.6    #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
     1.7 -  #> Sign.add_consts_i
     1.8 +  #> Sign.add_consts
     1.9        [(Binding.name "typeof", typ "'b => Type", NoSyn),
    1.10         (Binding.name "Type", typ "'a itself => Type", NoSyn),
    1.11         (Binding.name "Null", typ "Null", NoSyn),
    1.12 @@ -791,7 +791,7 @@
    1.13               val fu = Type.legacy_freeze u;
    1.14               val (def_thms, thy') = if t = nullt then ([], thy) else
    1.15                 thy
    1.16 -               |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
    1.17 +               |> Sign.add_consts [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
    1.18                 |> Global_Theory.add_defs false
    1.19                    [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
    1.20                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]