Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Boogie/Tools/boogie_loader.ML
changeset 35626 06197484c6ad
parent 35625 9c818cab0dd0
child 35682 5e6811f4294b 
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:19:47 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:47:02 2010 +0100
@@ -88,7 +88,7 @@
           let
             val args = Name.variant_list [] (replicate arity "'")
             val (T, thy') =
-              Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
+              Typedecl.typedecl (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
isabelle