diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal-General/nominal_library.ML	Wed Nov 10 13:46:21 2010 +0000
@@ -256,46 +256,24 @@
   end
 
 
-(** FIX: my_relation is necessary because of problem in Function Package *)
-
-fun inst_state_tac ctxt rel st =
-  let
-    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
-    val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
-  in case Term.add_vars (prop_of st') [] of
-       [v] => 
-         PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
-     | _ => Seq.empty
-  end
-
-fun my_relation_tac ctxt rel i =
-  TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN inst_state_tac ctxt rel
-
-(** FIX: end *)
-
-
-fun prove_termination_tac size_simps ctxt i st  =
+fun prove_termination_tac size_simps ctxt =
   let
     fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
         SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
       | mk_size_measure T = size_const T
 
-    val ((_ $ (_ $ rel)) :: _) = prems_of st
-    val measure_trm = 
-      fastype_of rel 
-      |> HOLogic.dest_setT
+    fun mk_measure_trm T = 
+      HOLogic.dest_setT T
+      |> fst o HOLogic.dest_prodT
       |> mk_size_measure 
       |> curry (op $) (Const (@{const_name measure}, dummyT))
       |> Syntax.check_term ctxt
+
     val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
       zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
-
   in
-    (*see above Function_Relation.relation_tac ctxt measure_trm*)
-    (my_relation_tac ctxt measure_trm
-     THEN_ALL_NEW  simp_tac ss) i st
+    Function_Relation.relation_tac ctxt mk_measure_trm
+    THEN_ALL_NEW simp_tac ss
   end
 
 fun prove_termination size_simps ctxt =