--- a/src/HOL/Tools/Function/size.ML Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML Sat Oct 17 16:58:03 2009 +0200
@@ -164,7 +164,7 @@
fun prove_unfolded_size_eqs size_ofp fs =
if null recTs2 then []
- else split_conj_thm (SkipProof.prove ctxt xs []
+ else split_conj_thm (Skip_Proof.prove ctxt xs []
(HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
@@ -198,7 +198,7 @@
fun prove_size_eqs p size_fns size_ofp simpset =
maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
+ map (fn constr => Drule.standard (Skip_Proof.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)