simplified '?' operator;
authorwenzelm
Tue Nov 28 00:35:18 2006 +0100 (2006-11-28)
changeset 21565bd28361f4c5b
parent 21564 519ee3129ee1
child 21566 af2932baf068
simplified '?' operator;
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typedef_package.ML
src/Pure/General/graph.ML
src/Pure/Isar/proof.ML
src/Pure/Syntax/parser.ML
src/Pure/Tools/class_package.ML
src/Pure/conjunction.ML
src/Pure/library.ML
src/Pure/meta_simplifier.ML
src/Pure/name.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Nov 27 23:48:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Nov 28 00:35:18 2006 +0100
     1.3 @@ -609,7 +609,7 @@
     1.4              then NONE else SOME (arity, (tyco, cs)))) insts;
     1.5        in
     1.6          thy
     1.7 -        |> K ((not o null) arities) ? (
     1.8 +        |> not (null arities) ? (
     1.9              f arities css
    1.10              #-> (fn defs =>
    1.11                ClassPackage.prove_instance_arity tac arities ("", []) defs
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Nov 27 23:48:10 2006 +0100
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Nov 28 00:35:18 2006 +0100
     2.3 @@ -54,9 +54,9 @@
     2.4        replicate (length args) HOLogic.typeS, HOLogic.typeS);
     2.5  
     2.6  fun add_typedecls decls thy =
     2.7 -  thy
     2.8 -  |> Theory.add_typedecls decls
     2.9 -  |> can (Theory.assert_super HOL.thy) ? fold HOL_arity decls;
    2.10 +  if can (Theory.assert_super HOL.thy) thy then
    2.11 +    thy |> Theory.add_typedecls decls |> fold HOL_arity decls
    2.12 +  else thy |> Theory.add_typedecls decls;
    2.13  
    2.14  
    2.15  
     3.1 --- a/src/Pure/General/graph.ML	Mon Nov 27 23:48:10 2006 +0100
     3.2 +++ b/src/Pure/General/graph.ML	Tue Nov 28 00:35:18 2006 +0100
     3.3 @@ -145,7 +145,7 @@
     3.4  fun project proj G =
     3.5    let
     3.6      fun subg (k, (i, (preds, succs))) =
     3.7 -      K (proj k) ? Table.update (k, (i, (filter proj preds, filter proj succs)));
     3.8 +      proj k ? Table.update (k, (i, (filter proj preds, filter proj succs)));
     3.9    in Graph (fold_graph subg G Table.empty) end;
    3.10  
    3.11  
     4.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 27 23:48:10 2006 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Tue Nov 28 00:35:18 2006 +0100
     4.3 @@ -776,13 +776,13 @@
     4.4      |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
     4.5      |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
     4.6      |> map_context (ProofContext.auto_bind_goal props)
     4.7 -    |> K chaining ? (`the_facts #-> using_facts)
     4.8 +    |> chaining ? (`the_facts #-> using_facts)
     4.9      |> put_facts NONE
    4.10      |> open_block
    4.11      |> put_goal NONE
    4.12      |> enter_backward
    4.13 -    |> K (not (null vars)) ? refine_terms (length propss')
    4.14 -    |> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd)
    4.15 +    |> not (null vars) ? refine_terms (length propss')
    4.16 +    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
    4.17    end;
    4.18  
    4.19  fun generic_qed state =
    4.20 @@ -915,7 +915,7 @@
    4.21    in
    4.22      state
    4.23      |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
    4.24 -    |> K int ? (fn goal_state =>
    4.25 +    |> int ? (fn goal_state =>
    4.26        (case test_proof goal_state of
    4.27          Result (SOME _) => goal_state
    4.28        | Result NONE => error (fail_msg (context_of goal_state))
     5.1 --- a/src/Pure/Syntax/parser.ML	Mon Nov 27 23:48:10 2006 +0100
     5.2 +++ b/src/Pure/Syntax/parser.ML	Tue Nov 28 00:35:18 2006 +0100
     5.3 @@ -278,7 +278,7 @@
     5.4                            else (new_prod :: tk_prods, true);
     5.5  
     5.6                          val prods' = prods
     5.7 -                                     |> K is_new' ? AList.update (op =) (tk, tk_prods');
     5.8 +                                     |> is_new' ? AList.update (op =) (tk, tk_prods');
     5.9                      in store tks prods' (is_new orelse is_new') end;
    5.10  
    5.11                  val (nt_prods', prod_count', changed) =
    5.12 @@ -367,7 +367,7 @@
    5.13  
    5.14                        val nt_prods' =
    5.15                          nt_prods'
    5.16 -                        |> (K (key = SOME UnknownStart)) ? AList.update (op =) (key, tk_prods')
    5.17 +                        |> (key = SOME UnknownStart) ? AList.update (op =) (key, tk_prods')
    5.18  
    5.19                        val added_tks =
    5.20                          subtract matching_tokens old_tks new_tks;
     6.1 --- a/src/Pure/Tools/class_package.ML	Mon Nov 27 23:48:10 2006 +0100
     6.2 +++ b/src/Pure/Tools/class_package.ML	Tue Nov 28 00:35:18 2006 +0100
     6.3 @@ -314,7 +314,7 @@
     6.4        supclasses
     6.5        |> map (#name_axclass o fst o the_class_data thy)
     6.6        |> Sign.certify_sort thy
     6.7 -      |> null ? K (Sign.defaultS thy);
     6.8 +      |> (fn [] => Sign.defaultS thy | S => S);    (* FIXME Why syntax defaultS? *)
     6.9      val expr_supclasses = Locale.Merge
    6.10        (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses);
    6.11      val expr = Locale.Merge (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses
     7.1 --- a/src/Pure/conjunction.ML	Mon Nov 27 23:48:10 2006 +0100
     7.2 +++ b/src/Pure/conjunction.ML	Tue Nov 28 00:35:18 2006 +0100
     7.3 @@ -216,7 +216,7 @@
     7.4      val intro =
     7.5        (eq RS Drule.equal_elim_rule2)
     7.6        |> curry n
     7.7 -      |> K (n = 0) ? Thm.eq_assumption 1;
     7.8 +      |> n = 0 ? Thm.eq_assumption 1;
     7.9      val dests = map (project (eq RS Drule.equal_elim_rule1)) (1 upto n);
    7.10    in (intro, dests) end;
    7.11  
     8.1 --- a/src/Pure/library.ML	Mon Nov 27 23:48:10 2006 +0100
     8.2 +++ b/src/Pure/library.ML	Tue Nov 28 00:35:18 2006 +0100
     8.3 @@ -24,7 +24,7 @@
     8.4    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
     8.5    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
     8.6    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
     8.7 -  val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
     8.8 +  val ? : bool * ('a -> 'a) -> 'a -> 'a
     8.9    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    8.10    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    8.11    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    8.12 @@ -271,7 +271,7 @@
    8.13  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    8.14  
    8.15  (*conditional application*)
    8.16 -fun b ? f = fn x => if b x then f x else x;
    8.17 +fun b ? f = fn x => if b then f x else x;
    8.18  
    8.19  (*composition with multiple args*)
    8.20  fun (f oo g) x y = f (g x y);
     9.1 --- a/src/Pure/meta_simplifier.ML	Mon Nov 27 23:48:10 2006 +0100
     9.2 +++ b/src/Pure/meta_simplifier.ML	Tue Nov 28 00:35:18 2006 +0100
     9.3 @@ -1223,11 +1223,11 @@
     9.4  
     9.5  local
     9.6  
     9.7 -fun gen_norm_hhf ss =
     9.8 -  (not o Drule.is_norm_hhf o Thm.prop_of) ?
     9.9 -    Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss)
    9.10 -  #> Thm.adjust_maxidx_thm ~1
    9.11 -  #> Drule.gen_all;
    9.12 +fun gen_norm_hhf ss th =
    9.13 +  (if Drule.is_norm_hhf (Thm.prop_of th) then th
    9.14 +   else Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
    9.15 +  |> Thm.adjust_maxidx_thm ~1
    9.16 +  |> Drule.gen_all;
    9.17  
    9.18  val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
    9.19  
    10.1 --- a/src/Pure/name.ML	Mon Nov 27 23:48:10 2006 +0100
    10.2 +++ b/src/Pure/name.ML	Tue Nov 28 00:35:18 2006 +0100
    10.3 @@ -123,7 +123,7 @@
    10.4            val x0 = Symbol.bump_init x;
    10.5            val x' = vary x0;
    10.6            val ctxt' = ctxt
    10.7 -            |> K (x0 <> x') ? declare_renaming (x0, x')
    10.8 +            |> x0 <> x' ? declare_renaming (x0, x')
    10.9              |> declare x';
   10.10          in (x', ctxt') end;
   10.11    in (x' ^ replicate_string n "_", ctxt') end);