src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

               ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
           binds = [], cases = []}) preds cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     val lthy'' = lthy'
       |> fold Variable.auto_fixes cases_rules
-      |> Proof_Context.update_cases true case_env
+      |> Proof_Context.update_cases case_env
     fun after_qed thms goal_ctxt =
       let
         val global_thms = Proof_Context.export goal_ctxt
           (Proof_Context.init_global (Proof_Context.theory_of goal_ctxt)) (map the_single thms)
       in