# HG changeset patch
# User wenzelm
# Date 1257874361 -3600
# Node ID d7784ad2680de0b95618ff7d832766164e1a8e4f
# Parent  702c2a771be6f31763816768401218f2d9db7e5d# Parent  a0a8a40385a2e689efa0107e9294264326b250c1
merged

diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Tue Nov 10 18:32:41 2009 +0100
@@ -64,7 +64,7 @@
         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     in
       thy
-      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
+      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
       |> snd
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/HOL.thy	Tue Nov 10 18:32:41 2009 +0100
@@ -2003,16 +2003,6 @@
 
 quickcheck_params [size = 5, iterations = 50]
 
-ML {*
-structure Quickcheck_RecFun_Simps = Named_Thms
-(
-  val name = "quickcheck_recfun_simp"
-  val description = "simplification rules of recursive functions as needed by Quickcheck"
-)
-*}
-
-setup Quickcheck_RecFun_Simps.setup
-
 
 subsubsection {* Nitpick setup *}
 
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Library/Float.thy	Tue Nov 10 18:32:41 2009 +0100
@@ -1378,8 +1378,8 @@
   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
   shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
 proof -
-  have "?lb \<le> ?ub" by (auto!)
-  have "0 \<le> ?lb" and "?lb \<noteq> 0" by (auto!)
+  have "?lb \<le> ?ub" using assms by auto
+  have "0 \<le> ?lb" and "?lb \<noteq> 0" using assms by auto
   have "?k * y \<le> ?x" using assms by auto
   also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`])
   also have "\<dots> \<le> real (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl)
@@ -1390,8 +1390,8 @@
   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
   shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
 proof -
-  have "?lb \<le> ?ub" by (auto!)
-  hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" by (auto!)
+  have "?lb \<le> ?ub" using assms by auto
+  hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" using assms by auto
   have "real (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl)
   also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`])
   also have "\<dots> \<le> ?k * y" using assms by auto
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -397,11 +397,8 @@
   Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
 
 val perm_simp_meth =
-  Args.bang_facts -- Scan.lift perm_simp_options --|
-  Method.sections (Simplifier.simp_modifiers') >>
-  (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
-    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-      (CHANGED_PROP oo tac) (simpset_of ctxt))));
+  Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
+  (fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac (simpset_of ctxt)));
 
 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
 fun local_simp_meth_setup tac =
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -349,7 +349,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> TheoryTarget.init name
+  |> Theory_Target.init name
   |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
   |> LocalTheory.exit_global;
 
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -411,7 +411,7 @@
         #> fold_rev Code.add_eqn thms);
   in
     thy
-    |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
+    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -37,8 +37,7 @@
 val simp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
      Code.add_default_eqn_attribute,
-     Nitpick_Simps.add,
-     Quickcheck_RecFun_Simps.add]
+     Nitpick_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -144,7 +144,7 @@
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
-      ||> TheoryTarget.instantiation
+      ||> Theory_Target.instantiation
            (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -65,8 +65,8 @@
 val setup =
   Arith_Facts.setup #>
   Method.setup @{binding arith}
-    (Args.bang_facts >> (fn prems => fn ctxt =>
-      METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+    (Scan.succeed (fn ctxt =>
+      METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
         THEN' verbose_arith_tac ctxt))))
     "various arithmetic decision procedures";
 
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -896,7 +896,7 @@
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> TheoryTarget.init NONE
+      |> Theory_Target.init NONE
       |> LocalTheory.set_group group
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> LocalTheory.exit;
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -924,9 +924,9 @@
   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup @{binding linarith}
-    (Args.bang_facts >> (fn prems => fn ctxt =>
+    (Scan.succeed (fn ctxt =>
       METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+        HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" gen_tac;
 
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -270,9 +270,9 @@
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
       (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
-    fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"),
-      map (Attrib.internal o K)
-        [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]);
+    fun simp_attr_binding prefix =
+      (Binding.qualify true prefix (Binding.name "simps"),
+        map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial ())
@@ -293,14 +293,14 @@
 
 fun add_primrec_global fixes specs thy =
   let
-    val lthy = TheoryTarget.init NONE thy;
+    val lthy = Theory_Target.init NONE thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in (simps', LocalTheory.exit_global lthy') end;
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
-    val lthy = TheoryTarget.overloading ops thy;
+    val lthy = Theory_Target.overloading ops thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in (simps', LocalTheory.exit_global lthy') end;
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -82,7 +82,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in   
     thy
-    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+    |> Theory_Target.instantiation ([tyco], vs, @{sort random})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
@@ -216,8 +216,7 @@
     |-> (fn proto_simps => prove_simps proto_simps)
     |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)
-          [Simplifier.simp_add, Nitpick_Simps.add, Quickcheck_RecFun_Simps.add]),
-            simps))
+          [Simplifier.simp_add, Nitpick_Simps.add]), simps))
     |> snd
   end
 
@@ -301,7 +300,7 @@
       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   in
     thy
-    |> TheoryTarget.instantiation (tycos, vs, @{sort random})
+    |> Theory_Target.instantiation (tycos, vs, @{sort random})
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/recdef.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -201,8 +201,9 @@
         tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
-    val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Simps.add,
-      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else [];
+    val simp_att =
+      if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
+      else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -113,7 +113,7 @@
     thy
     |> Code.add_datatype [constr]
     |> Code.add_eqn proj_eq
-    |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
+    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition
          (NONE, (Attrib.empty_binding, eq)))
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Transcendental.thy	Tue Nov 10 18:32:41 2009 +0100
@@ -25,7 +25,7 @@
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
 by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
-         del: setsum_op_ivl_Suc cong: strong_setsum_cong)
+         del: setsum_op_ivl_Suc)
 
 lemma lemma_realpow_diff_sumr2:
   fixes y :: "'a::{comm_ring,monoid_mult}" shows
@@ -1981,11 +1981,11 @@
 lemma cos_monotone_0_pi: assumes "0 \<le> y" and "y < x" and "x \<le> pi"
   shows "cos x < cos y"
 proof -
-  have "- (x - y) < 0" by (auto!)
+  have "- (x - y) < 0" using assms by auto
 
   from MVT2[OF `y < x` DERIV_cos[THEN impI, THEN allI]]
   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z" by auto
-  hence "0 < z" and "z < pi" by (auto!)
+  hence "0 < z" and "z < pi" using assms by auto
   hence "0 < sin z" using sin_gt_zero_pi by auto
   hence "cos x - cos y < 0" unfolding cos_diff minus_mult_commute[symmetric] using `- (x - y) < 0` by (rule mult_pos_neg2)
   thus ?thesis by auto
@@ -2002,7 +2002,7 @@
 lemma cos_monotone_minus_pi_0: assumes "-pi \<le> y" and "y < x" and "x \<le> 0"
   shows "cos y < cos x"
 proof -
-  have "0 \<le> -x" and "-x < -y" and "-y \<le> pi" by (auto!)
+  have "0 \<le> -x" and "-x < -y" and "-y \<le> pi" using assms by auto
   from cos_monotone_0_pi[OF this]
   show ?thesis unfolding cos_minus .
 qed
@@ -2017,7 +2017,8 @@
 
 lemma sin_monotone_2pi': assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2" shows "sin y \<le> sin x"
 proof -
-  have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi" using pi_ge_two by (auto!)
+  have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
+    using pi_ge_two and assms by auto
   from cos_monotone_0_pi'[OF this] show ?thesis unfolding minus_sin_cos_eq[symmetric] by auto
 qed
 
@@ -2179,14 +2180,14 @@
   have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse (cos x'^2)"
   proof (rule allI, rule impI)
     fix x' :: real assume "y \<le> x' \<and> x' \<le> x"
-    hence "-(pi/2) < x'" and "x' < pi/2" by (auto!)
+    hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto
     from cos_gt_zero_pi[OF this]
     have "cos x' \<noteq> 0" by auto
     thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan)
   qed
   from MVT2[OF `y < x` this] 
   obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<twosuperior>)" by auto
-  hence "- (pi / 2) < z" and "z < pi / 2" by (auto!)
+  hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
   hence "0 < cos z" using cos_gt_zero_pi by auto
   hence inv_pos: "0 < inverse ((cos z)\<twosuperior>)" by auto
   have "0 < x - y" using `y < x` by auto
diff -r 702c2a771be6 -r d7784ad2680d src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOL/Typerep.thy	Tue Nov 10 18:32:41 2009 +0100
@@ -50,7 +50,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
-    |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
+    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd
diff -r 702c2a771be6 -r d7784ad2680d src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -75,7 +75,7 @@
         val ((_, {type_definition, set_def, ...}), thy2) = thy1
           |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
         val lthy3 = thy2
-          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
+          |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
         val below_def' = Syntax.check_term lthy3 below_def;
         val ((_, (_, below_definition')), lthy4) = lthy3
           |> Specification.definition (NONE,
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/General/symbol.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -18,7 +18,6 @@
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
   val is_utf8_trailer: symbol -> bool
-  val name_of: symbol -> string
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
@@ -137,10 +136,6 @@
 fun is_regular s =
   not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
 
-fun name_of s = if is_symbolic s
-  then (unsuffix ">" o unprefix "\\<") s
-  else error (malformed_msg s);
-
 
 (* ascii symbols *)
 
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/args.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -223,7 +223,7 @@
 
 val bang_facts = Scan.peek (fn context =>
   P.position ($$$ "!") >> (fn (_, pos) =>
-    (warning ("use of prems in proof method" ^ Position.str_of pos);
+    (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos);
       Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
 
 val from_to =
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/class.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -290,7 +290,7 @@
        Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
          (*FIXME should not modify base_morph, although admissible*)
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
-    |> TheoryTarget.init (SOME class)
+    |> Theory_Target.init (SOME class)
     |> pair class
   end;
 
@@ -310,7 +310,7 @@
   let
     val thy = ProofContext.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub = case TheoryTarget.peek lthy
+    val proto_sub = case Theory_Target.peek lthy
      of {is_class = false, ...} => error "Not in a class context"
       | {target, ...} => target;
     val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
@@ -323,7 +323,7 @@
     fun after_qed some_wit =
       ProofContext.theory (register_subclass (sub, sup)
         some_dep_morph some_wit export)
-      #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
+      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
   in do_proof after_qed some_prop goal_ctxt end;
 
 fun user_proof after_qed some_prop =
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -774,7 +774,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
-      |> TheoryTarget.init (SOME name)
+      |> Theory_Target.init (SOME name)
       |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
@@ -842,7 +842,7 @@
 fun gen_sublocale prep_expr intern raw_target expression thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = TheoryTarget.init (SOME target) thy;
+    val target_ctxt = Theory_Target.init (SOME target) thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     fun after_qed witss = ProofContext.theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -390,7 +390,7 @@
 val _ =
   OuterSyntax.command "context" "enter local theory context" K.thy_decl
     (P.name --| P.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name)));
+      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
 
 
 (* locales *)
@@ -452,7 +452,7 @@
   OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
    (P.multi_arity --| P.begin
      >> (fn arities => Toplevel.print o
-         Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities)));
+         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
 
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
@@ -470,7 +470,7 @@
       Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
       >> P.triple1) --| P.begin
    >> (fn operations => Toplevel.print o
-         Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
+         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
 
 
 (* code generation *)
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -19,7 +19,7 @@
   val overloading_cmd: (string * string * bool) list -> theory -> local_theory
 end;
 
-structure TheoryTarget: THEORY_TARGET =
+structure Theory_Target: THEORY_TARGET =
 struct
 
 (* context data *)
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -103,7 +103,7 @@
 
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
-val loc_init = TheoryTarget.context;
+val loc_init = Theory_Target.context;
 val loc_exit = LocalTheory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
@@ -192,7 +192,7 @@
 
 (* print state *)
 
-val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
+val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
 
 fun print_state_context state =
   (case try node_of state of
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/name.ML
--- a/src/Pure/name.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/name.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -152,7 +152,8 @@
   | desymbolize upper s =
       let
         val xs as (x :: _) = Symbol.explode s;
-        val ys = if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
+        val ys =
+          if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
           else "x" :: xs;
         fun is_valid x =
           Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
@@ -161,15 +162,17 @@
           | sep xs = "_" :: xs;
         fun desep ("_" :: xs) = xs
           | desep xs = xs;
-        fun desymb x xs = if is_valid x
-            then x :: xs
-          else if Symbol.is_symbolic x
-            then "_" :: explode (Symbol.name_of x) @ sep xs
+        fun desymb x xs =
+          if is_valid x then x :: xs
           else
-            sep xs
-        fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
-          else (if forall Symbol.is_ascii_upper cs
-            then map else nth_map 0) Symbol.to_ascii_lower cs;
+            (case Symbol.decode x of
+              Symbol.Sym name => "_" :: explode name @ sep xs
+            | _ => sep xs);
+        fun upper_lower cs =
+          if upper then nth_map 0 Symbol.to_ascii_upper cs
+          else
+            (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
+              Symbol.to_ascii_lower cs;
       in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
 
 end;
diff -r 702c2a771be6 -r d7784ad2680d src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Pure/simplifier.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -189,8 +189,7 @@
         in Variable.export_terms ctxt' lthy lhss' end
         |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
        proc = proc,
-       identifier = identifier}
-      |> morph_simproc (LocalTheory.target_morphism lthy);
+       identifier = identifier};
   in
     lthy |> LocalTheory.declaration false (fn phi =>
       let
diff -r 702c2a771be6 -r d7784ad2680d src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Tue Nov 10 16:12:35 2009 +0100
+++ b/src/Tools/intuitionistic.ML	Tue Nov 10 18:32:41 2009 +0100
@@ -87,11 +87,9 @@
 
 fun method_setup name =
   Method.setup name
-    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
-      Method.sections modifiers >>
-      (fn (prems, n) => fn ctxt => METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (prems @ facts) THEN'
-        ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))))
+    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
+      (fn opt_lim => fn ctxt =>
+        SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
     "intuitionistic proof search";
 
 end;