src/Pure/Proof/extraction.ML

     val _ = name <> "" orelse error "add_expand_thms: unnamed theorem";
 
     val is_def =
       (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
          (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
-           andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
+           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
        | _ => false) handle TERM _ => false;
   in
     (ExtractionData.put (if is_def then
         {realizes_eqns = realizes_eqns,
          typeof_eqns = add_rule (([],