src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     HOLogic.mk_Trueprop
       (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
   end;
 
 (* special setup for simpset *)                  
-val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
+val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
 
 (* Definition of executable functions and their intro and elim rules *)
 

   (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   in
      (* make this simpset better! *)
     asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
     THEN print_tac' options "after prove_match:"
-    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
+    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
            THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
            THEN print_tac' options "if condition to be solved:"
            THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:"))
            THEN check_format thy
            THEN print_tac' options "after if simplification - a TRY block")))

         (all_input_of T))
         preds
   in 
     (* remove not_False_eq_True when simpset in prove_match is better *)
     simp_tac (HOL_basic_ss addsimps
-      (@{thms "HOL.simp_thms"} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
+      (@{thms HOL.simp_thms} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
     (* need better control here! *)
   end
 
 fun prove_clause options thy nargs modes mode (_, clauses) (ts, moded_ps) =
   let

     fn prem => fn additional_arguments =>
     let
       val [polarity, depth] = additional_arguments
       val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
       val depth' =
-        Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
-          $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})
+        Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
     in [polarity', depth'] end
   }
 
 val random_comp_modifiers = Comp_Mod.Comp_Modifiers
   {