--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 16:26:48 2012 +0200
@@ -86,7 +86,7 @@
let
val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
in
- [quot_thm, thm] MRSL @{thm apply_rsp''}
+ [quot_thm, thm] MRSL @{thm apply_rspQ3''}
end
in
fold disch_arg ty_args rsp_thm
@@ -101,11 +101,11 @@
let
val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
- val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
+ val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs}
val abs_rep_eq =
case (HOLogic.dest_Trueprop o prop_of) fun_rel of
Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
- | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
+ | Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
| _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
val unabs_def = unabs_all_def ctxt unfolded_def