src/HOL/Decision_Procs/mir_tac.ML

        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac mir_ss 1)]
       (Thm.trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
-        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+        Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
     let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty
              then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
              else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))