# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1334070650 -3600
# Node ID d53e422e06f2dff7998918b3676dc02bf24cb47d
# Parent  b2eafae4d40109acb221924b2f8e7b92d492a172
moved lift_raw_const wrapper out of the Quotient-package into Nominal2

diff -r b2eafae4d401 -r d53e422e06f2 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Apr 10 16:50:30 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Apr 10 16:10:50 2012 +0100
@@ -18,8 +18,6 @@
     (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
     local_theory -> Proof.state
 
-  val lift_raw_const: typ list -> (string * term * mixfix) -> thm -> local_theory ->
-    Quotient_Info.quotconsts * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -331,27 +329,6 @@
 val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
 
 
-(* a wrapper for automatically lifting a raw constant *)
-fun lift_raw_const qtys (qconst_name, rconst, mx') rsp_thm lthy =
-  let
-    val rty = fastype_of rconst
-    val qty = Quotient_Term.derive_qtyp lthy qtys rty
-    val lhs_raw = Free (qconst_name, qty)
-    val rhs_raw = rconst
-
-    val raw_var = (Binding.name qconst_name, NONE, mx')
-    val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
-    val lhs = Syntax.check_term ctxt lhs_raw
-    val rhs = Syntax.check_term ctxt rhs_raw
-
-    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
-    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
-    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
-
-  in
-    add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm  ctxt
-  end
-
 (* parser and command *)
 val quotdef_parser =
   Scan.option Parse_Spec.constdecl --