# HG changeset patch
# User wenzelm
# Date 1428498403 -7200
# Node ID d69dc7a133e76c8109e3d1a136f727cfcfaacf5c
# Parent  3d207f8f40dd49b1255b9272e0369e48c7de9d5f
more standard access to specific subgoal;

diff -r 3d207f8f40dd -r d69dc7a133e7 src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Wed Apr 08 11:52:53 2015 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Wed Apr 08 15:06:43 2015 +0200
@@ -10,40 +10,42 @@
   val relation_infer_tac: Proof.context -> term -> int -> tactic
 end
 
-structure Function_Relation : FUNCTION_RELATION =
+structure Function_Relation: FUNCTION_RELATION =
 struct
 
 (* tactic version *)
 
-fun inst_state_tac ctxt inst st =
-  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
-    [v as (_, T)] =>
-      PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) st
-  | _ => Seq.empty);
+fun inst_state_tac ctxt inst =
+  SUBGOAL (fn (goal, _) =>
+    (case Term.add_vars goal [] of
+      [v as (_, T)] =>
+        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))]))
+    | _ => no_tac));
 
 fun relation_tac ctxt rel i =
   TRY (Function_Common.termination_rule_tac ctxt i)
-  THEN inst_state_tac ctxt rel;
+  THEN inst_state_tac ctxt rel i;
 
 
 (* version with type inference *)
 
-fun inst_state_infer_tac ctxt rel st =
-  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
-    [v as (_, T)] =>
-      let
-        val rel' = singleton (Variable.polymorphic ctxt) rel
-          |> map_types Type_Infer.paramify_vars
-          |> Type.constraint T
-          |> Syntax.check_term ctxt
-          |> Thm.cterm_of ctxt;
-      in
-        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), rel')])) st
-      end
-  | _ => Seq.empty);
+fun inst_state_infer_tac ctxt rel =
+  SUBGOAL (fn (goal, _) =>
+    (case Term.add_vars goal [] of
+      [v as (_, T)] =>
+        let
+          val rel' =
+            singleton (Variable.polymorphic ctxt) rel
+            |> map_types Type_Infer.paramify_vars
+            |> Type.constraint T
+            |> Syntax.check_term ctxt;
+        in
+          PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')]))
+        end
+    | _ => no_tac));
 
 fun relation_infer_tac ctxt rel i =
   TRY (Function_Common.termination_rule_tac ctxt i)
-  THEN inst_state_infer_tac ctxt rel;
+  THEN inst_state_infer_tac ctxt rel i;
 
 end