# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1377869737 -3600
# Node ID 8c53bcd5c0aec72e41715bb896b3117e4c583f89
# Parent  ea327a4c4f437debec999a9fe11574a0b35fff27
updated to lates Isabelle

diff -r ea327a4c4f43 -r 8c53bcd5c0ae Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Wed Jul 31 13:15:29 2013 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Fri Aug 30 14:35:37 2013 +0100
@@ -364,8 +364,8 @@
 fun 
   compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
 where
-  "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
-| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
+  "\<theta>1 \<circ> [] = \<theta>1"
+| "\<theta>1 \<circ> ((X,T)#\<theta>2) = (X,\<theta>1<T>)#(\<theta>1 \<circ> \<theta>2)"
 
 lemma compose_ty:
   fixes  \<theta>1 \<theta>2 :: "Subst"
diff -r ea327a4c4f43 -r 8c53bcd5c0ae Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Wed Jul 31 13:15:29 2013 +0100
+++ b/Nominal/nominal_induct.ML	Fri Aug 30 14:35:37 2013 +0100
@@ -173,8 +173,9 @@
 in
 
 val nominal_induct_method =
-  Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
-  avoiding -- fixing -- rule_spec) >>
+  Scan.lift (Args.mode Induct.no_simpN) -- 
+    (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
+      avoiding -- fixing -- rule_spec) >>
   (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
     RAW_METHOD_CASES (fn facts =>
       HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));