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