--- 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
--- 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;
--- 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;
--- 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))
--- 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;
--- 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
--- 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;
--- 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);
--- 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];
--- 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);