1.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Wed Apr 04 10:38:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Wed Apr 04 13:41:38 2012 +0200
     1.3 @@ -106,13 +106,13 @@
     1.4      (domain_type abs_type, range_type abs_type)
     1.5    end
     1.6  
     1.7 -fun prove_quot_theorem ctxt (rty, qty) =
     1.8 +fun prove_quot_theorem' ctxt (rty, qty) =
     1.9    case (rty, qty) of
    1.10      (Type (s, tys), Type (s', tys')) =>
    1.11        if s = s'
    1.12        then
    1.13          let
    1.14 -          val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
    1.15 +          val args = map (prove_quot_theorem' ctxt) (tys ~~ tys')
    1.16          in
    1.17            if forall is_id_quot args
    1.18            then
    1.19 @@ -126,7 +126,7 @@
    1.20            val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
    1.21            val qtyenv = match ctxt equiv_match_err qty_pat qty
    1.22            val rtys' = map (Envir.subst_type qtyenv) rtys
    1.23 -          val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
    1.24 +          val args = map (prove_quot_theorem' ctxt) (tys ~~ rtys')
    1.25          in
    1.26            if forall is_id_quot args
    1.27            then
    1.28 @@ -152,22 +152,18 @@
    1.29      Thm.instantiate (ty_inst, []) quot_thm
    1.30    end
    1.31  
    1.32 -fun absrep_fun ctxt (rty, qty) = 
    1.33 +fun prove_quot_theorem ctxt (rty, qty) =
    1.34    let
    1.35      val thy = Proof_Context.theory_of ctxt
    1.36 -    val quot_thm = prove_quot_theorem ctxt (rty, qty)
    1.37 -    val forced_quot_thm = force_qty_type thy qty quot_thm
    1.38 +    val quot_thm = prove_quot_theorem' ctxt (rty, qty)
    1.39    in
    1.40 -    quot_thm_abs forced_quot_thm
    1.41 +    force_qty_type thy qty quot_thm
    1.42    end
    1.43  
    1.44 +fun absrep_fun ctxt (rty, qty) =
    1.45 +  quot_thm_abs (prove_quot_theorem ctxt (rty, qty))
    1.46 +
    1.47  fun equiv_relation ctxt (rty, qty) =
    1.48 -  let
    1.49 -    val thy = Proof_Context.theory_of ctxt
    1.50 -    val quot_thm = prove_quot_theorem ctxt (rty, qty)
    1.51 -    val forced_quot_thm = force_qty_type thy qty quot_thm
    1.52 -  in
    1.53 -    quot_thm_rel forced_quot_thm
    1.54 -  end
    1.55 +  quot_thm_rel (prove_quot_theorem ctxt (rty, qty))
    1.56  
    1.57  end;