--- a/src/HOL/Tools/Function/size.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML Sat Oct 17 00:52:37 2009 +0200
@@ -198,7 +198,7 @@
fun prove_size_eqs p size_fns size_ofp simpset =
maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => standard (SkipProof.prove ctxt [] []
+ map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
(gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
size_ofp size_const T constr)
(fn _ => simp_tac simpset 1))) constrs)