# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289128951 0
# Node ID 781fbc8c05916752f63f86813037c34bd885c1d6
# Parent  8ed62410236edffd36d32154b429e914e4f79da6
fixed locally the problem with the function package; all tests work again

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
 
diff -r 8ed62410236e -r 781fbc8c0591 Nominal/Ex/Datatypes.thy
--- a/Nominal/Ex/Datatypes.thy	Sat Nov 06 06:18:41 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy	Sun Nov 07 11:22:31 2010 +0000
@@ -7,7 +7,7 @@
   atom_decl - example by John Matthews
 *)
 
-(* FIXME: throws an problem with fv-function
+
 nominal_datatype 'a Maybe = 
   Nothing 
 | Just 'a
@@ -23,7 +23,6 @@
 thm Maybe.fv_bn_eqvt
 thm Maybe.size_eqvt
 thm Maybe.supp
-*)
 
 (*
   using a datatype inside a nominal_datatype
diff -r 8ed62410236e -r 781fbc8c0591 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Sat Nov 06 06:18:41 2010 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Sun Nov 07 11:22:31 2010 +0000
@@ -8,7 +8,6 @@
 class s1
 class s2
 
-(* FIXME
 nominal_datatype ('a, 'b) lam =
   Var "name"
 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
@@ -23,7 +22,7 @@
 thm lam.eq_iff
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
-*)
+
 
 end