# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1372669018 -3600
# Node ID 87dbeba4b25a22cdac48f8068f1f08f90b33124b
# Parent  e5d9b6bca88cde81be52cf7029773cde3c2522f4
updated to ne Isabelle

diff -r e5d9b6bca88c -r 87dbeba4b25a Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Jun 04 09:39:23 2013 +0100
+++ b/Nominal/nominal_function_core.ML	Mon Jul 01 09:56:58 2013 +0100
@@ -577,13 +577,13 @@
       |> Thm.implies_intr (ihyp)
       |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
       |> Thm.forall_intr (cterm_of thy x)
-      |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+      |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
     val goalstate =  
          Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt 
       |> Thm.close_derivation
-      |> Goal.protect
+      |> Goal.protect 0
       |> fold_rev (Thm.implies_intr o cprop_of) compat
       |> Thm.implies_intr (cprop_of complete)
       |> Thm.implies_intr (cprop_of invariant)
@@ -970,7 +970,7 @@
     |> (fn it => it COMP accI)
     |> Thm.implies_intr ihyp
     |> Thm.forall_intr (cterm_of thy x)
-    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+    |> (fn it => Drule.compose (it, 2, wf_induct_rule))
     |> curry op RS (Thm.assume wfR')
     |> forall_intr_vars
     |> (fn it => it COMP allI)