author kuncar Tue Mar 27 14:46:34 2012 +0200 (2012-03-27) changeset 47156 861f53bd95fe parent 47133 89b13238d7f2 child 47157 2b0749c80bc8
note a code eqn in quotient_def
```     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.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'')
```