src/Provers/classical.ML
changeset 15703 727ef1b8b3ee
parent 15574 b1d1b5bfc464
child 15707 80b421d8a8be
--- a/src/Provers/classical.ML	Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Provers/classical.ML	Wed Apr 13 18:34:22 2005 +0200
@@ -168,8 +168,8 @@
   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
-  val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
-  val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
+  val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
+  val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
   val setup: (theory -> theory) list
 
   val get_delta_claset: ProofContext.context -> claset