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/Tools/Function/size.ML
changeset 33553 35f2b30593a8
parent 33522 737589bb9bb8
child 33671 4b0f2599ed48 
--- a/src/HOL/Tools/Function/size.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -144,7 +144,7 @@
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
-      ||> TheoryTarget.instantiation
+      ||> Theory_Target.instantiation
            (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
isabelle