default abstypes and default abstract equations make technical (no_code) annotation superfluous

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Feb 06 17:57:03 2015 +0100
@@ -1592,7 +1592,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \<newline>
+    @@{command (HOL) setup_lifting} \<newline>
       @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
   \<close>}
 
@@ -1645,9 +1645,6 @@
     The command @{command (HOL) "setup_lifting"} also sets up the code generator
     for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"},
     the Lifting package proves and registers a code equation (if there is one) for the new constant.
-    If the option @{text "no_code"} is specified, the Lifting package does not set up the code
-    generator and as a consequence no code equations involving an abstract type are registered
-    by @{command (HOL) "lift_definition"}.
 
   \item @{command (HOL) "lift_definition"} @{text "f :: \<tau>"} @{keyword (HOL) "is"} @{text t}
     Defines a new function @{text f} with an abstract type @{text \<tau>}

--- a/src/HOL/Code_Numeral.thy	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Feb 06 17:57:03 2015 +0100
@@ -13,7 +13,7 @@
 typedef integer = "UNIV \<Colon> int set"
   morphisms int_of_integer integer_of_int ..
 
-setup_lifting (no_code) type_definition_integer
+setup_lifting type_definition_integer
 
 lemma integer_eq_iff:
   "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
@@ -620,7 +620,7 @@
 typedef natural = "UNIV \<Colon> nat set"
   morphisms nat_of_natural natural_of_nat ..
 
-setup_lifting (no_code) type_definition_natural
+setup_lifting type_definition_natural
 
 lemma natural_eq_iff [termination_simp]:
   "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"

--- a/src/HOL/Library/AList_Mapping.thy	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Library/AList_Mapping.thy	Fri Feb 06 17:57:03 2015 +0100
@@ -66,5 +66,6 @@
 lemma [code nbe]:
   "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
   by (fact equal_refl)
-  
+
 end
+

--- a/src/HOL/Library/Float.thy	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Library/Float.thy	Fri Feb 06 17:57:03 2015 +0100
@@ -27,7 +27,7 @@
 lemma type_definition_float': "type_definition real float_of float"
   using type_definition_float unfolding real_of_float_def .
 
-setup_lifting (no_code) type_definition_float'
+setup_lifting type_definition_float'
 
 lemmas float_of_inject[simp]
 

--- a/src/HOL/Library/Polynomial.thy	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Feb 06 17:57:03 2015 +0100
@@ -93,7 +93,7 @@
   morphisms coeff Abs_poly
   unfolding almost_everywhere_zero_def by auto
 
-setup_lifting (no_code) type_definition_poly
+setup_lifting type_definition_poly
 
 lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
   by (simp add: coeff_inject [symmetric] fun_eq_iff)

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Feb 06 17:57:03 2015 +0100
@@ -8,9 +8,9 @@
 sig
   exception SETUP_LIFTING_INFR of string
 
-  val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
+  val setup_by_quotient: thm -> thm option -> thm option -> local_theory -> local_theory
 
-  val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
+  val setup_by_typedef_thm: thm -> local_theory -> local_theory
 
   val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
 end
@@ -138,22 +138,22 @@
   end
 end
 
-fun define_code_constr gen_code quot_thm lthy =
+fun define_code_constr quot_thm lthy =
   let
     val abs = quot_thm_abs quot_thm
   in
-    if gen_code andalso is_Const abs then
+    if is_Const abs then
       let
-        val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
+        val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy
       in  
-         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
+         Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy'
       end
     else
       lthy
   end
 
-fun define_abs_type gen_code quot_thm lthy =
-  if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
+fun define_abs_type quot_thm lthy =
+  if Lifting_Def.can_generate_code_cert quot_thm then
     let
       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
       val add_abstype_attribute = 
@@ -232,7 +232,7 @@
       |> Bundle.bundle ((binding, [restore_lifting_att])) []
   end
 
-fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
+fun setup_lifting_infr quot_thm opt_reflp_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
     val (_, qty) = quot_thm_rty_qty quot_thm
@@ -254,17 +254,14 @@
       SOME reflp_thm => lthy
         |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
               [reflp_thm RS @{thm reflp_ge_eq}])
-        |> define_code_constr gen_code quot_thm
+        |> define_code_constr quot_thm
       | NONE => lthy
-        |> define_abs_type gen_code quot_thm
-    fun declare_no_code qty =  Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Lifting_Info.add_no_code_type (Morphism.typ phi qty |> Tname))
+        |> define_abs_type quot_thm
   in
     lthy
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
       |> lifting_bundle qty_full_name quotients
-      |> (if not gen_code then declare_no_code qty else I)
   end
 
 local
@@ -476,15 +473,13 @@
 (*
   Sets up the Lifting package by a quotient theorem.
 
-  gen_code - flag if an abstract type given by quot_thm should be registred 
-    as an abstract type in the code generator
   quot_thm - a quotient theorem (Quotient R Abs Rep T)
   opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
     (in the form "reflp R")
   opt_par_thm - a parametricity theorem for R
 *)
 
-fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
+fun setup_by_quotient quot_thm opt_reflp_thm opt_par_thm lthy =
   let
     (**)
     val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
@@ -612,7 +607,7 @@
                                                      else setup_transfer_rules_nonpar lthy
   in
     lthy
-      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+      |> setup_lifting_infr quot_thm opt_reflp_thm
       |> setup_transfer_rules
   end
 
@@ -624,7 +619,7 @@
   typedef_thm - a typedef theorem (type_definition Rep Abs S)
 *)
 
-fun setup_by_typedef_thm gen_code typedef_thm lthy =
+fun setup_by_typedef_thm typedef_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add)
@@ -737,11 +732,11 @@
     lthy
       |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
             [quot_thm])
-      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+      |> setup_lifting_infr quot_thm opt_reflp_thm
       |> setup_transfer_rules
   end
 
-fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
+fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy =
   let 
     val input_thm = singleton (Attrib.eval_thms lthy) xthm
     val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
@@ -768,7 +763,7 @@
         val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
         val _ = check_qty (snd (quot_thm_rty_qty input_thm))
       in
-        setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
+        setup_by_quotient input_thm opt_reflp_thm opt_par_thm lthy
       end
 
     fun setup_typedef () = 
@@ -781,7 +776,7 @@
           | NONE => (
             case opt_par_xthm of
               SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
-              | NONE => setup_by_typedef_thm gen_code input_thm lthy
+              | NONE => setup_by_typedef_thm input_thm lthy
           )
       end
   in
@@ -791,16 +786,13 @@
       | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   end
 
-val opt_gen_code =
-  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
-
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "setup lifting infrastructure" 
-      (opt_gen_code -- Parse.xthm -- Scan.option Parse.xthm 
+      (Parse.xthm -- Scan.option Parse.xthm 
       -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
-        (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
-          setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
+        (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => 
+          setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
 
 (* restoring lifting infrastructure *)
 

--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Feb 06 17:57:03 2015 +0100
@@ -7,12 +7,12 @@
 signature QUOTIENT_TYPE =
 sig
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option * bool * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
+    ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
 
   val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
+    ((binding * binding) option * thm option) -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
+  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
     (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
 end;
 
@@ -110,7 +110,7 @@
     (def_thm, lthy'')
   end;
 
-fun setup_lifting_package gen_code quot3_thm equiv_thm opt_par_thm lthy =
+fun setup_lifting_package quot3_thm equiv_thm opt_par_thm lthy =
   let
     val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
     val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
@@ -128,11 +128,11 @@
       )
   in
     lthy'
-      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm opt_par_thm
+      |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm opt_par_thm
       |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 
-fun init_quotient_infr gen_code quot_thm equiv_thm opt_par_thm lthy =
+fun init_quotient_infr quot_thm equiv_thm opt_par_thm lthy =
   let
     val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
     val (qtyp, rtyp) = (dest_funT o fastype_of) rep
@@ -147,11 +147,11 @@
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Quotient_Info.update_quotients (qty_full_name, quot_info phi)
           #> Quotient_Info.update_abs_rep (qty_full_name, abs_rep_info phi))
-      |> setup_lifting_package gen_code quot_thm equiv_thm opt_par_thm
+      |> setup_lifting_package quot_thm equiv_thm opt_par_thm
   end
 
 (* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
   let
     val part_equiv =
       if partial
@@ -203,7 +203,7 @@
       quot_thm = quotient_thm}
 
     val lthy4 = lthy3
-      |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
+      |> init_quotient_infr quotient_thm equiv_thm opt_par_thm
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
           if partial then [] else @{attributes [quot_equiv]}),
@@ -313,7 +313,7 @@
 
 fun quotient_type_cmd spec lthy =
   let
-    fun parse_spec (((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
+    fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
       let
         val rty = Syntax.read_typ lthy rty_str
         val tmp_lthy1 = Variable.declare_typ rty lthy
@@ -324,7 +324,7 @@
         val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
         val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
       in
-        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), tmp_lthy2)
+        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), tmp_lthy2)
       end
 
     val (spec', _) = parse_spec spec lthy
@@ -332,13 +332,10 @@
     quotient_type spec' lthy
   end
 
-val opt_gen_code =
-  Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true
-
 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
 
 val quotspec_parser =
-     (opt_gen_code -- Parse.type_args -- Parse.binding) --
+     (Parse.type_args -- Parse.binding) --
       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
       Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
         (@{keyword "/"} |-- (partial -- Parse.term))  --

--- a/src/HOL/Word/Word.thy	Fri Feb 06 19:17:17 2015 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 06 17:57:03 2015 +0100
@@ -187,7 +187,7 @@
   "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   by (simp add: reflp_def)
 
-setup_lifting (no_code) Quotient_word reflp_word
+setup_lifting Quotient_word reflp_word
 
 text {* TODO: The next lemma could be generated automatically. *}