--- a/Attic/Quot/quotient_def.ML	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*  Title:      HOL/Tools/Quotient/quotient_def.thy
-    Author:     Cezary Kaliszyk and Christian Urban
-
-Definitions for constants on quotient types.
-*)
-
-signature QUOTIENT_DEF =
-sig
-  val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
-    local_theory -> (term * thm) * local_theory
-
-  val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
-    local_theory -> (term * thm) * local_theory
-
-  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
-end;
-
-structure Quotient_Def: QUOTIENT_DEF =
-struct
-
-open Quotient_Info;
-open Quotient_Term;
-
-(** Interface and Syntax Setup **)
-
-(* The ML-interface for a quotient definition takes
-   as argument:
-
-    - an optional binding and mixfix annotation
-    - attributes
-    - the new constant as term
-    - the rhs of the definition as term
-
-   It returns the defined constant and its definition
-   theorem; stores the data in the qconsts data slot.
-
-   Restriction: At the moment the right-hand side of the
-   definition must be a constant. Similarly the left-hand 
-   side must be a constant.
-*)
-fun error_msg bind str = 
-let 
-  val name = Binding.name_of bind
-  val pos = Position.str_of (Binding.pos_of bind)
-in
-  error ("Head of quotient_definition " ^ 
-    (quote str) ^ " differs from declaration " ^ name ^ pos)
-end
-
-fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
-let
-  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"
-  
-  fun sanity_test NONE _ = true
-    | sanity_test (SOME bind) str =
-        if Name.of_binding bind = str then true
-        else error_msg bind str
-
-  val _ = sanity_test optbind lhs_str
-
-  val qconst_bname = Binding.name lhs_str
-  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
-  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
-  val (_, prop') = Local_Defs.cert_def lthy prop
-  val (_, newrhs) = Primitive_Defs.abs_def prop'
-
-  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
-
-  (* data storage *)
-  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
-  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
-  val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
-in
-  ((trm, thm), lthy'')
-end
-
-fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
-let
-  val lhs = Syntax.read_term lthy lhs_str
-  val rhs = Syntax.read_term lthy rhs_str
-  val lthy' = Variable.declare_term lhs lthy
-  val lthy'' = Variable.declare_term rhs lthy'
-in
-  quotient_def (decl, (attr, (lhs, rhs))) lthy''
-end
-
-fun quotient_lift_const (b, t) ctxt =
-  quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
-    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
-
-local
-  structure P = OuterParse;
-in
-
-val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
-
-val quotdef_parser =
-  Scan.optional quotdef_decl (NONE, NoSyn) -- 
-    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
-end
-
-val _ =
-  OuterSyntax.local_theory "quotient_definition"
-    "definition for constants over the quotient type"
-      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
-
-end; (* structure *)