# HG changeset patch
# User wenzelm
# Date 1164670518 -3600
# Node ID bd28361f4c5b67f755638e4acca22a3d481efe37
# Parent  519ee3129ee1f1ac822cb11eb97fbbae7fc4bbd4
simplified '?' operator;

diff -r 519ee3129ee1 -r bd28361f4c5b src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -609,7 +609,7 @@
             then NONE else SOME (arity, (tyco, cs)))) insts;
       in
         thy
-        |> K ((not o null) arities) ? (
+        |> not (null arities) ? (
             f arities css
             #-> (fn defs =>
               ClassPackage.prove_instance_arity tac arities ("", []) defs
diff -r 519ee3129ee1 -r bd28361f4c5b src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -54,9 +54,9 @@
       replicate (length args) HOLogic.typeS, HOLogic.typeS);
 
 fun add_typedecls decls thy =
-  thy
-  |> Theory.add_typedecls decls
-  |> can (Theory.assert_super HOL.thy) ? fold HOL_arity decls;
+  if can (Theory.assert_super HOL.thy) thy then
+    thy |> Theory.add_typedecls decls |> fold HOL_arity decls
+  else thy |> Theory.add_typedecls decls;
 
 
 
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/General/graph.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -145,7 +145,7 @@
 fun project proj G =
   let
     fun subg (k, (i, (preds, succs))) =
-      K (proj k) ? Table.update (k, (i, (filter proj preds, filter proj succs)));
+      proj k ? Table.update (k, (i, (filter proj preds, filter proj succs)));
   in Graph (fold_graph subg G Table.empty) end;
 
 
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -776,13 +776,13 @@
     |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
     |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
     |> map_context (ProofContext.auto_bind_goal props)
-    |> K chaining ? (`the_facts #-> using_facts)
+    |> chaining ? (`the_facts #-> using_facts)
     |> put_facts NONE
     |> open_block
     |> put_goal NONE
     |> enter_backward
-    |> K (not (null vars)) ? refine_terms (length propss')
-    |> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+    |> not (null vars) ? refine_terms (length propss')
+    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;
 
 fun generic_qed state =
@@ -915,7 +915,7 @@
   in
     state
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
-    |> K int ? (fn goal_state =>
+    |> int ? (fn goal_state =>
       (case test_proof goal_state of
         Result (SOME _) => goal_state
       | Result NONE => error (fail_msg (context_of goal_state))
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -278,7 +278,7 @@
                           else (new_prod :: tk_prods, true);
 
                         val prods' = prods
-                                     |> K is_new' ? AList.update (op =) (tk, tk_prods');
+                                     |> is_new' ? AList.update (op =) (tk, tk_prods');
                     in store tks prods' (is_new orelse is_new') end;
 
                 val (nt_prods', prod_count', changed) =
@@ -367,7 +367,7 @@
 
                       val nt_prods' =
                         nt_prods'
-                        |> (K (key = SOME UnknownStart)) ? AList.update (op =) (key, tk_prods')
+                        |> (key = SOME UnknownStart) ? AList.update (op =) (key, tk_prods')
 
                       val added_tks =
                         subtract matching_tokens old_tks new_tks;
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -314,7 +314,7 @@
       supclasses
       |> map (#name_axclass o fst o the_class_data thy)
       |> Sign.certify_sort thy
-      |> null ? K (Sign.defaultS thy);
+      |> (fn [] => Sign.defaultS thy | S => S);    (* FIXME Why syntax defaultS? *)
     val expr_supclasses = Locale.Merge
       (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses);
     val expr = Locale.Merge (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/conjunction.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -216,7 +216,7 @@
     val intro =
       (eq RS Drule.equal_elim_rule2)
       |> curry n
-      |> K (n = 0) ? Thm.eq_assumption 1;
+      |> n = 0 ? Thm.eq_assumption 1;
     val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
   in (intro, dests) end;
 
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/library.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -24,7 +24,7 @@
   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
-  val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
+  val ? : bool * ('a -> 'a) -> 'a -> 'a
   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
@@ -271,7 +271,7 @@
 fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
 
 (*conditional application*)
-fun b ? f = fn x => if b x then f x else x;
+fun b ? f = fn x => if b then f x else x;
 
 (*composition with multiple args*)
 fun (f oo g) x y = f (g x y);
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -1223,11 +1223,11 @@
 
 local
 
-fun gen_norm_hhf ss =
-  (not o Drule.is_norm_hhf o Thm.prop_of) ?
-    Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss)
-  #> Thm.adjust_maxidx_thm ~1
-  #> Drule.gen_all;
+fun gen_norm_hhf ss th =
+  (if Drule.is_norm_hhf (Thm.prop_of th) then th
+   else Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
+  |> Thm.adjust_maxidx_thm ~1
+  |> Drule.gen_all;
 
 val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
 
diff -r 519ee3129ee1 -r bd28361f4c5b src/Pure/name.ML
--- a/src/Pure/name.ML	Mon Nov 27 23:48:10 2006 +0100
+++ b/src/Pure/name.ML	Tue Nov 28 00:35:18 2006 +0100
@@ -123,7 +123,7 @@
           val x0 = Symbol.bump_init x;
           val x' = vary x0;
           val ctxt' = ctxt
-            |> K (x0 <> x') ? declare_renaming (x0, x')
+            |> x0 <> x' ? declare_renaming (x0, x')
             |> declare x';
         in (x', ctxt') end;
   in (x' ^ replicate_string n "_", ctxt') end);