src/HOL/Tools/res_axioms.ML
changeset 27809 a1e409db516b
parent 27330 1af2598b5f7d
child 27865 27a8ad9612a3
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Sat Aug 09 12:28:13 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sat Aug 09 22:43:46 2008 +0200
     1.3 @@ -557,7 +557,7 @@
     1.4  
     1.5  (** Attribute for converting a theorem into clauses **)
     1.6  
     1.7 -val clausify = Attrib.syntax (Scan.lift Args.nat
     1.8 +val clausify = Attrib.syntax (Scan.lift OuterParse.nat
     1.9    >> (fn i => Thm.rule_attribute (fn context => fn th =>
    1.10        Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
    1.11