1.1 --- a/src/HOL/Library/Float.thy	Thu Apr 19 17:31:34 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Apr 19 18:24:40 2012 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  lemma type_definition_float': "type_definition real float_of float"
     1.5    using type_definition_float unfolding real_of_float_def .
     1.6  
     1.7 -setup_lifting (no_code) type_definition_float'
     1.8 +setup_lifting (no_abs_code) type_definition_float'
     1.9  
    1.10  lemmas float_of_inject[simp]
    1.11  

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 17:31:34 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 18:24:40 2012 +0200
     2.3 @@ -38,8 +38,8 @@
     2.4      (def_thm, lthy'')
     2.5    end
     2.6  
     2.7 -fun define_abs_type no_code quot_thm lthy =
     2.8 -  if not no_code andalso Lifting_Def.can_generate_code_cert quot_thm then
     2.9 +fun define_abs_type no_abs_code quot_thm lthy =
    2.10 +  if not no_abs_code andalso Lifting_Def.can_generate_code_cert quot_thm then
    2.11      let
    2.12        val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
    2.13        val add_abstype_attribute = 
    2.14 @@ -78,7 +78,7 @@
    2.15                                                  @ (map Pretty.string_of errs)))
    2.16    end
    2.17  
    2.18 -fun setup_lifting_infr no_code quot_thm lthy =
    2.19 +fun setup_lifting_infr no_abs_code quot_thm lthy =
    2.20    let
    2.21      val _ = quot_thm_sanity_check lthy quot_thm
    2.22      val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
    2.23 @@ -89,10 +89,10 @@
    2.24      lthy
    2.25        |> Local_Theory.declaration {syntax = false, pervasive = true}
    2.26          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
    2.27 -      |> define_abs_type no_code quot_thm
    2.28 +      |> define_abs_type no_abs_code quot_thm
    2.29    end
    2.30  
    2.31 -fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy =
    2.32 +fun setup_by_quotient no_abs_code quot_thm maybe_reflp_thm lthy =
    2.33    let
    2.34      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    2.35      val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
    2.36 @@ -124,10 +124,10 @@
    2.37          [quot_thm RS @{thm Quotient_right_total}])
    2.38        |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
    2.39          [quot_thm RS @{thm Quotient_rel_eq_transfer}])
    2.40 -      |> setup_lifting_infr no_code quot_thm
    2.41 +      |> setup_lifting_infr no_abs_code quot_thm
    2.42    end
    2.43  
    2.44 -fun setup_by_typedef_thm no_code typedef_thm lthy =
    2.45 +fun setup_by_typedef_thm no_abs_code typedef_thm lthy =
    2.46    let
    2.47      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
    2.48      val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
    2.49 @@ -174,10 +174,10 @@
    2.50          [[quot_thm] MRSL @{thm Quotient_right_unique}])
    2.51        |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
    2.52          [[quot_thm] MRSL @{thm Quotient_right_total}])
    2.53 -      |> setup_lifting_infr no_code quot_thm
    2.54 +      |> setup_lifting_infr no_abs_code quot_thm
    2.55    end
    2.56  
    2.57 -fun setup_lifting_cmd no_code xthm opt_reflp_xthm lthy =
    2.58 +fun setup_lifting_cmd no_abs_code xthm opt_reflp_xthm lthy =
    2.59    let 
    2.60      val input_thm = singleton (Attrib.eval_thms lthy) xthm
    2.61      val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
    2.62 @@ -200,14 +200,14 @@
    2.63              val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
    2.64              val _ = sanity_check_reflp_thm reflp_thm
    2.65            in
    2.66 -            setup_by_quotient no_code input_thm (SOME reflp_thm) lthy
    2.67 +            setup_by_quotient no_abs_code input_thm (SOME reflp_thm) lthy
    2.68            end
    2.69 -        | NONE => setup_by_quotient no_code input_thm NONE lthy
    2.70 +        | NONE => setup_by_quotient no_abs_code input_thm NONE lthy
    2.71  
    2.72      fun setup_typedef () = 
    2.73        case opt_reflp_xthm of
    2.74          SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
    2.75 -        | NONE => setup_by_typedef_thm no_code input_thm lthy
    2.76 +        | NONE => setup_by_typedef_thm no_abs_code input_thm lthy
    2.77    in
    2.78      case input_term of
    2.79        (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
    2.80 @@ -215,12 +215,12 @@
    2.81        | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
    2.82    end
    2.83  
    2.84 -val opt_no_code =
    2.85 -  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K true) --| @{keyword ")"})) false
    2.86 +val opt_no_abs_code =
    2.87 +  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_abs_code" >> K true) --| @{keyword ")"})) false
    2.88  
    2.89  val _ = 
    2.90    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
    2.91      "Setup lifting infrastructure" 
    2.92 -      (opt_no_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
    2.93 -        (fn ((no_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_code xthm opt_reflp_xthm))
    2.94 +      (opt_no_abs_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
    2.95 +        (fn ((no_abs_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_abs_code xthm opt_reflp_xthm))
    2.96  end;