--- 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"

--- 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)));