# HG changeset patch
# User urbanc
# Date 1137001159 -3600
# Node ID 9968dc816cda3a778aa24b0346d4b167c4e1e320
# Parent  2ff0ae57431d47a9b0ae9d874d002ee49bc6e4ba
cahges to use the new induction-principle (now proved in
full glory)

diff -r 2ff0ae57431d -r 9968dc816cda src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Jan 11 18:38:32 2006 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Jan 11 18:39:19 2006 +0100
@@ -455,7 +455,7 @@
   and b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
-proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
+proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
   case (Forall X T\<^isub>1 T\<^isub>2)
   have ih_T\<^isub>1: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>1 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact 
   have ih_T\<^isub>2: "\<And>\<Gamma>. \<turnstile> \<Gamma> ok \<Longrightarrow> T\<^isub>2 closed_in \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
@@ -478,7 +478,7 @@
   and     b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
-apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct_unsafe)
+apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
 apply(auto simp add: ty.supp abs_supp closed_in_def supp_atm)
   --{* Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used