diff -r 8ed62410236e -r 781fbc8c0591 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sat Nov 06 06:18:41 2010 +0000
+++ b/Nominal-General/nominal_library.ML	Sun Nov 07 11:22:31 2010 +0000
@@ -255,6 +255,27 @@
       THEN ALLGOALS (asm_full_simp_tac simp_set)
   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  =
   let
     fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
@@ -270,8 +291,10 @@
       |> 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
-    (Function_Relation.relation_tac ctxt measure_trm
+    (*see above Function_Relation.relation_tac ctxt measure_trm*)
+    (my_relation_tac ctxt measure_trm
      THEN_ALL_NEW  simp_tac ss) i st
   end