fixed section syntax;

--- a/src/Provers/classical.ML	Wed Mar 08 23:46:59 2000 +0100
+++ b/src/Provers/classical.ML	Wed Mar 08 23:47:44 2000 +0100
@@ -1021,8 +1021,11 @@
 val delN = "del";
 val delruleN = "delrule";
 
+val colon = Args.$$$ ":";
 val query = Args.$$$ "?";
 val qquery = Args.$$$ "??";
+val query_colon = Args.$$$ "?:";
+val qquery_colon = Args.$$$ "??:";
 
 fun cla_att change xtra haz safe = Attrib.syntax
   (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change));
@@ -1133,16 +1136,16 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- qquery >> K ((I, xtra_dest_local):Method.modifier),
-  Args.$$$ destN -- query >> K (I, haz_dest_local),
-  Args.$$$ destN >> K (I, safe_dest_local),
-  Args.$$$ elimN -- qquery >> K (I, xtra_elim_local),
-  Args.$$$ elimN -- query >> K (I, haz_elim_local),
-  Args.$$$ elimN >> K (I, safe_elim_local),
-  Args.$$$ introN -- qquery >> K (I, xtra_intro_local),
-  Args.$$$ introN -- query >> K (I, haz_intro_local),
-  Args.$$$ introN >> K (I, safe_intro_local),
-  Args.$$$ delN >> K (I, delrule_local)];
+ [Args.$$$ destN -- qquery_colon >> K ((I, xtra_dest_local):Method.modifier),
+  Args.$$$ destN -- query_colon >> K (I, haz_dest_local),
+  Args.$$$ destN -- colon >> K (I, safe_dest_local),
+  Args.$$$ elimN -- qquery_colon >> K (I, xtra_elim_local),
+  Args.$$$ elimN -- query_colon >> K (I, haz_elim_local),
+  Args.$$$ elimN -- colon >> K (I, safe_elim_local),
+  Args.$$$ introN -- qquery_colon >> K (I, xtra_intro_local),
+  Args.$$$ introN -- query_colon >> K (I, haz_intro_local),
+  Args.$$$ introN -- colon >> K (I, safe_intro_local),
+  Args.$$$ delN -- colon >> K (I, delrule_local)];
 
 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));

--- a/src/Provers/simplifier.ML	Wed Mar 08 23:46:59 2000 +0100
+++ b/src/Provers/simplifier.ML	Wed Mar 08 23:47:44 2000 +0100
@@ -474,17 +474,19 @@
 
 (* simplification *)
 
+val colon = Args.$$$ ":";
+
 val simp_modifiers =
- [Args.$$$ simpN -- Args.$$$ addN >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ delN >> K (I, simp_del_local),
-  Args.$$$ simpN -- Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
-  Args.$$$ otherN >> K (I, I)];
+ [Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
+  Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local),
+  Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
+  Args.$$$ otherN -- colon >> K (I, I)];
 
 val simp_modifiers' =
- [Args.$$$ addN >> K (I, simp_add_local),
-  Args.$$$ delN >> K (I, simp_del_local),
-  Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
-  Args.$$$ otherN >> K (I, I)];
+ [Args.$$$ addN -- colon >> K (I, simp_add_local),
+  Args.$$$ delN -- colon >> K (I, simp_del_local),
+  Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
+  Args.$$$ otherN -- colon >> K (I, I)];
 
 fun simp_method tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>