1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Mar 22 20:42:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Mar 22 21:40:19 2014 +0100
     1.3 @@ -85,16 +85,16 @@
     1.4    val eq_OO_meta = mk_meta_eq @{thm eq_OO} 
     1.5  
     1.6    fun print_generate_pcr_cr_eq_error ctxt term = 
     1.7 -  let
     1.8 -    val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
     1.9 -    val error_msg = cat_lines 
    1.10 -      ["Generation of a pcr_cr_eq failed.",
    1.11 -      (Pretty.string_of (Pretty.block
    1.12 -         [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
    1.13 -       "Most probably a relator_eq rule for one of the involved types is missing."]
    1.14 -  in
    1.15 -    error error_msg
    1.16 -  end
    1.17 +    let
    1.18 +      val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT)
    1.19 +      val error_msg = cat_lines 
    1.20 +        ["Generation of a pcr_cr_eq failed.",
    1.21 +        (Pretty.string_of (Pretty.block
    1.22 +           [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
    1.23 +         "Most probably a relator_eq rule for one of the involved types is missing."]
    1.24 +    in
    1.25 +      error error_msg
    1.26 +    end
    1.27  in
    1.28    fun define_pcr_cr_eq lthy pcr_rel_def =
    1.29      let
    1.30 @@ -121,15 +121,15 @@
    1.31            (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
    1.32    in
    1.33      case (term_of o Thm.rhs_of) pcr_cr_eq of
    1.34 -      Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ => 
    1.35 +      Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ =>
    1.36          let
    1.37            val thm = 
    1.38              pcr_cr_eq
    1.39              |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
    1.40              |> mk_HOL_eq
    1.41              |> singleton (Variable.export lthy orig_lthy)
    1.42 -          val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), 
    1.43 -            [thm]) lthy
    1.44 +          val ((_, [thm]), lthy) =
    1.45 +            Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) lthy
    1.46          in
    1.47            (thm, lthy)
    1.48          end
    1.49 @@ -626,7 +626,7 @@
    1.50      val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
    1.51      (**)    
    1.52      val quot_thm = case typedef_set of
    1.53 -      Const ("Orderings.top_class.top", _) => 
    1.54 +      Const (@{const_name top}, _) => 
    1.55          [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
    1.56        | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
    1.57          [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
    1.58 @@ -638,7 +638,7 @@
    1.59      fun qualify suffix = Binding.qualified true suffix qty_name
    1.60      val opt_reflp_thm = 
    1.61        case typedef_set of
    1.62 -        Const ("Orderings.top_class.top", _) => 
    1.63 +        Const (@{const_name top}, _) => 
    1.64            SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
    1.65          | _ =>  NONE
    1.66      val dom_thm = get_Domainp_thm quot_thm
    1.67 @@ -819,7 +819,7 @@
    1.68                      Pretty.brk 1,
    1.69                      Display.pretty_thm ctxt pcr_cr_eq]]
    1.70              val (pcr_const_eq, eqs) = strip_comb eq_lhs
    1.71 -            fun is_eq (Const ("HOL.eq", _)) = true
    1.72 +            fun is_eq (Const (@{const_name HOL.eq}, _)) = true
    1.73                | is_eq _ = false
    1.74              fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
    1.75                | eq_Const _ _ = false