1.1 --- a/src/HOL/Orderings.thy	Sun Jul 26 22:24:13 2009 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sun Jul 26 22:28:31 2009 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  theory Orderings
     1.6  imports HOL
     1.7 -uses "~~/src/Provers/order.ML"
     1.8 +uses
     1.9 +  "~~/src/Provers/order.ML"
    1.10 +  "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    1.11  begin
    1.12  
    1.13  subsection {* Quasi orders *}
    1.14 @@ -289,7 +291,7 @@
    1.15  sig
    1.16    val print_structures: Proof.context -> unit
    1.17    val setup: theory -> theory
    1.18 -  val order_tac: thm list -> Proof.context -> int -> tactic
    1.19 +  val order_tac: Proof.context -> thm list -> int -> tactic
    1.20  end;
    1.21  
    1.22  structure Orders: ORDERS =
    1.23 @@ -329,7 +331,7 @@
    1.24  
    1.25  (** Method **)
    1.26  
    1.27 -fun struct_tac ((s, [eq, le, less]), thms) prems =
    1.28 +fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
    1.29    let
    1.30      fun decomp thy (@{const Trueprop} $ t) =
    1.31        let
    1.32 @@ -354,13 +356,13 @@
    1.33        | decomp thy _ = NONE;
    1.34    in
    1.35      case s of
    1.36 -      "order" => Order_Tac.partial_tac decomp thms prems
    1.37 -    | "linorder" => Order_Tac.linear_tac decomp thms prems
    1.38 +      "order" => Order_Tac.partial_tac decomp thms ctxt prems
    1.39 +    | "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
    1.40      | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
    1.41    end
    1.42  
    1.43 -fun order_tac prems ctxt =
    1.44 -  FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt)));
    1.45 +fun order_tac ctxt prems =
    1.46 +  FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
    1.47  
    1.48  
    1.49  (** Attribute **)
    1.50 @@ -394,7 +396,7 @@
    1.51  (** Setup **)
    1.52  
    1.53  val setup =
    1.54 -  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
    1.55 +  Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
    1.56      "transitivity reasoner" #>
    1.57    attrib_setup;
    1.58  
    1.59 @@ -532,7 +534,7 @@
    1.60        Simplifier.simproc thy name raw_ts proc) procs)) thy;
    1.61  fun add_solver name tac =
    1.62    Simplifier.map_simpset (fn ss => ss addSolver
    1.63 -    mk_solver' name (fn ss => tac (Simplifier.prems_of_ss ss) (Simplifier.the_context ss)));
    1.64 +    mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)));
    1.65  
    1.66  in
    1.67    add_simprocs [