1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Mar 26 21:03:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Mar 27 14:46:34 2012 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4      simplify_code_eq ctxt code_cert
     1.5    end
     1.6  
     1.7 -fun define_code_cert def_thm rsp_thm (rty, qty) lthy = 
     1.8 +fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
     1.9    let
    1.10      val quot_thm = Quotient_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
    1.11    in
    1.12 @@ -129,27 +129,27 @@
    1.13          val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
    1.14        in
    1.15          lthy
    1.16 -          |> (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert])
    1.17 +          |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert])
    1.18        end
    1.19      else
    1.20        lthy
    1.21    end
    1.22  
    1.23 -fun define_code_eq def_thm lthy =
    1.24 +fun define_code_eq code_eqn_thm_name def_thm lthy =
    1.25    let
    1.26      val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
    1.27      val code_eq = unabs_all_def lthy unfolded_def
    1.28      val simp_code_eq = simplify_code_eq lthy code_eq
    1.29    in
    1.30      lthy
    1.31 -      |> (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [simp_code_eq])
    1.32 +      |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
    1.33    end
    1.34  
    1.35 -fun define_code def_thm rsp_thm (rty, qty) lthy =
    1.36 +fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
    1.37    if body_type rty = body_type qty then 
    1.38 -    define_code_eq def_thm lthy
    1.39 +    define_code_eq code_eqn_thm_name def_thm lthy
    1.40    else 
    1.41 -    define_code_cert def_thm rsp_thm (rty, qty) lthy
    1.42 +    define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
    1.43  
    1.44  (* The ML-interface for a quotient definition takes
    1.45     as argument:
    1.46 @@ -189,7 +189,9 @@
    1.47  
    1.48      (* data storage *)
    1.49      val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
    1.50 -    fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name
    1.51 +    val lhs_name = #1 var
    1.52 +    val rsp_thm_name = Binding.suffix_name "_rsp" lhs_name
    1.53 +    val code_eqn_thm_name = Binding.suffix_name "_code_eqn" lhs_name
    1.54      
    1.55      val lthy'' = lthy'
    1.56        |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.57 @@ -199,9 +201,9 @@
    1.58                Quotient_Info.update_quotconsts c qcinfo
    1.59            | _ => I))
    1.60        |> (snd oo Local_Theory.note) 
    1.61 -        ((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
    1.62 +        ((rsp_thm_name, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
    1.63          [rsp_thm])
    1.64 -      |> define_code def_thm rsp_thm (rty, qty)
    1.65 +      |> define_code code_eqn_thm_name def_thm rsp_thm (rty, qty)
    1.66  
    1.67    in
    1.68      (qconst_data, lthy'')