diff -r 6a6827bad05f -r 87806301a813 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sun Jul 26 22:24:13 2009 +0200 +++ b/src/HOL/Orderings.thy Sun Jul 26 22:28:31 2009 +0200 @@ -6,7 +6,9 @@ theory Orderings imports HOL -uses "~~/src/Provers/order.ML" +uses + "~~/src/Provers/order.ML" + "~~/src/Provers/quasi.ML" (* FIXME unused? *) begin subsection {* Quasi orders *} @@ -289,7 +291,7 @@ sig val print_structures: Proof.context -> unit val setup: theory -> theory - val order_tac: thm list -> Proof.context -> int -> tactic + val order_tac: Proof.context -> thm list -> int -> tactic end; structure Orders: ORDERS = @@ -329,7 +331,7 @@ (** Method **) -fun struct_tac ((s, [eq, le, less]), thms) prems = +fun struct_tac ((s, [eq, le, less]), thms) ctxt prems = let fun decomp thy (@{const Trueprop} \$ t) = let @@ -354,13 +356,13 @@ | decomp thy _ = NONE; in case s of - "order" => Order_Tac.partial_tac decomp thms prems - | "linorder" => Order_Tac.linear_tac decomp thms prems + "order" => Order_Tac.partial_tac decomp thms ctxt prems + | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.") end -fun order_tac prems ctxt = - FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt))); +fun order_tac ctxt prems = + FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt))); (** Attribute **) @@ -394,7 +396,7 @@ (** Setup **) val setup = - Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) + Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt []))) "transitivity reasoner" #> attrib_setup; @@ -532,7 +534,7 @@ Simplifier.simproc thy name raw_ts proc) procs)) thy; fun add_solver name tac = Simplifier.map_simpset (fn ss => ss addSolver - mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss))); + mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss))); in add_simprocs [