src/HOL/Tools/inductive_set_package.ML

 (***********************************************************************************)
 
 val anyt = Free ("t", TFree ("'t", []));
 
 fun strong_ind_simproc tab =
-  Simplifier.simproc_i HOL.thy "strong_ind" [anyt] (fn thy => fn ss => fn t =>
+  Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
     let
       fun close p t f =
         let val vs = Term.add_vars t []
         in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
           (p (fold (Logic.all o Var) vs t) f)

     SOME (SOME _) => true | _ => false;
 
 fun to_pred_simproc rules =
   let val rules' = map mk_meta_eq rules
   in
-    Simplifier.simproc_i HOL.thy "to_pred" [anyt]
+    Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
       (fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
   end;
 
 fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
     NONE => NONE