src/HOL/Tools/Function/size.ML
changeset 32970 fbd2bb2489a8
parent 32957 675c0c7e6a37
child 33056 791a4655cae3
     1.1 --- a/src/HOL/Tools/Function/size.ML	Sat Oct 17 16:40:41 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/size.ML	Sat Oct 17 16:58:03 2009 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  
     1.5      fun prove_unfolded_size_eqs size_ofp fs =
     1.6        if null recTs2 then []
     1.7 -      else split_conj_thm (SkipProof.prove ctxt xs []
     1.8 +      else split_conj_thm (Skip_Proof.prove ctxt xs []
     1.9          (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
    1.10             map (mk_unfolded_size_eq (AList.lookup op =
    1.11                 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
    1.12 @@ -198,7 +198,7 @@
    1.13  
    1.14      fun prove_size_eqs p size_fns size_ofp simpset =
    1.15        maps (fn (((_, (_, _, constrs)), size_const), T) =>
    1.16 -        map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
    1.17 +        map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] []
    1.18            (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
    1.19               size_ofp size_const T constr)
    1.20            (fn _ => simp_tac simpset 1))) constrs)