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 38348 cf7b2121ad9d
parent 36610 bafd82950e24
child 39557 fe5722fce758 
--- a/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -145,7 +145,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)))
-      ||> Theory_Target.instantiation
+      ||> Class.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