# HG changeset patch
# User urbanc
# Date 1131579386 -3600
# Node ID a51ab415209752e02b1db1762b8c2f19ddf150e1
# Parent  89e2e8bed08f2fba8c728cd9438000363f0af89c
called the induction principle "unsafe" instead of "test".

diff -r 89e2e8bed08f -r a51ab4152097 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 09 18:01:33 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Nov 10 00:36:26 2005 +0100
@@ -1088,7 +1088,7 @@
             (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
         end) (atoms ~~ finite_supp_thms) |>>
       Theory.add_path big_name |>>>
-      PureThy.add_axioms_i [(("induct_test", induct), [case_names_induct])] |>>
+      PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] |>>
       Theory.parent_path;
 
   in