src/HOL/Tools/Function/size.ML
changeset 32957 675c0c7e6a37
parent 32727 9072201cd69d
child 32970 fbd2bb2489a8
     1.1 --- a/src/HOL/Tools/Function/size.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/size.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  
     1.5      fun prove_size_eqs p size_fns size_ofp simpset =
     1.6        maps (fn (((_, (_, _, constrs)), size_const), T) =>
     1.7 -        map (fn constr => standard (SkipProof.prove ctxt [] []
     1.8 +        map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
     1.9            (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
    1.10               size_ofp size_const T constr)
    1.11            (fn _ => simp_tac simpset 1))) constrs)