# HG changeset patch
# User wenzelm
# Date 1329245499 -3600
# Node ID 61c7214b4885506d8d7a28e2d34152d9ebaaed06
# Parent  5ba52c337cd03b6dbc040229dd049b972046d0c3
tuned signature, according to actual usage of these operations;

diff -r 5ba52c337cd0 -r 61c7214b4885 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Feb 14 19:29:54 2012 +0100
+++ b/src/Pure/Isar/method.ML	Tue Feb 14 19:51:39 2012 +0100
@@ -4,16 +4,8 @@
 Isar proof methods.
 *)
 
-signature BASIC_METHOD =
-sig
-  val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-  val rule_trace: bool Config.T
-end;
-
 signature METHOD =
 sig
-  include BASIC_METHOD
   type method
   val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
   val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
@@ -42,6 +34,7 @@
   val all_assm_tac: Proof.context -> tactic
   val assumption: Proof.context -> method
   val close: bool -> Proof.context -> method
+  val rule_trace: bool Config.T
   val trace: Proof.context -> thm list -> unit
   val rule_tac: thm list -> thm list -> int -> tactic
   val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
@@ -89,18 +82,6 @@
 structure Method: METHOD =
 struct
 
-(** generic tools **)
-
-(* goal addressing *)
-
-fun FINDGOAL tac st =
-  let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
-  in find 1 (Thm.nprems_of st) st end;
-
-fun HEADGOAL tac = tac 1;
-
-
-
 (** proof methods **)
 
 (* datatype method *)
@@ -483,9 +464,6 @@
 
 end;
 
-structure Basic_Method: BASIC_METHOD = Method;
-open Basic_Method;
-
 val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
 val RAW_METHOD = Method.RAW_METHOD;
 val METHOD_CASES = Method.METHOD_CASES;
diff -r 5ba52c337cd0 -r 61c7214b4885 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Feb 14 19:29:54 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Feb 14 19:51:39 2012 +0100
@@ -36,7 +36,6 @@
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
   val refine_insert: thm list -> state -> state
-  val goal_tac: thm -> int -> tactic
   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
@@ -444,6 +443,8 @@
 
 (* refine via sub-proof *)
 
+local
+
 fun finish_tac 0 = K all_tac
   | finish_tac n =
       Goal.norm_hhf_tac THEN'
@@ -457,6 +458,12 @@
   Tactic.rtac rule THEN'
   finish_tac (Thm.nprems_of rule);
 
+fun FINDGOAL tac st =
+  let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
+  in find 1 (Thm.nprems_of st) st end;
+
+in
+
 fun refine_goals print_rule inner raw_rules state =
   let
     val (outer, (_, goal)) = get_goal state;
@@ -467,6 +474,8 @@
     |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
   end;
 
+end;
+
 
 (* conclude_goal *)
 
diff -r 5ba52c337cd0 -r 61c7214b4885 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Tue Feb 14 19:29:54 2012 +0100
+++ b/src/Pure/tactical.ML	Tue Feb 14 19:51:39 2012 +0100
@@ -48,6 +48,7 @@
   val ALLGOALS: (int -> tactic) -> tactic
   val SOMEGOAL: (int -> tactic) -> tactic
   val FIRSTGOAL: (int -> tactic) -> tactic
+  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
   val REPEAT_SOME: (int -> tactic) -> tactic
   val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
   val REPEAT_FIRST: (int -> tactic) -> tactic
@@ -314,6 +315,9 @@
   let fun find (i,n) = if i>n then no_tac else  tac(i) ORELSE find (i+1,n)
   in  find(1, nprems_of st)st  end;
 
+(*First subgoal only.*)
+fun HEADGOAL tac = tac 1;
+
 (*Repeatedly solve some using tac. *)
 fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
 fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));