Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typedecl.typedecl_global;
authorwenzelm
Tue, 09 Mar 2010 23:32:49 +0100
changeset 35682 5e6811f4294b
parent 35681 8b22a498b034
child 35686 abf91fba0a70
Typedecl.typedecl_global;
src/HOL/Boogie/Tools/boogie_loader.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/typedef.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Tue Mar 09 23:32:13 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Tue Mar 09 23:32:49 2010 +0100
@@ -88,7 +88,7 @@
           let
             val args = Name.variant_list [] (replicate arity "'")
             val (T, thy') =
-              Typedecl.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
+              Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
             val type_name = fst (Term.dest_Type T)
           in (((name, type_name), log_new name type_name), thy') end)
     end
--- a/src/HOL/Tools/typedef.ML	Tue Mar 09 23:32:13 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Tue Mar 09 23:32:49 2010 +0100
@@ -130,7 +130,7 @@
           in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
-      Typedecl.typedecl (tname, vs, mx)
+      Typedecl.typedecl_global (tname, vs, mx)
       #> snd
       #> Sign.add_consts_i
         [(Rep_name, newT --> oldT, NoSyn),
isabelle