src/Pure/Isar/specification.ML

             val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
           in
             ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
             ctxt' |> Variable.auto_fixes asm
             |> ProofContext.add_assms_i Assumption.assume_export
-              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
+              [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)
           end;
 
         val atts = map (Attrib.internal o K)
           [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];