# HG changeset patch
# User wenzelm
# Date 1119298444 -7200
# Node ID e10b0d5fa33a85c76dbbd6de3b9a9df1cfd32670
# Parent  f66ab8a4e98f4c22bfc2cda79950dd286b03d00d
tuned;

diff -r f66ab8a4e98f -r e10b0d5fa33a src/Pure/Isar/proof_history.ML
--- a/src/Pure/Isar/proof_history.ML	Mon Jun 20 22:14:03 2005 +0200
+++ b/src/Pure/Isar/proof_history.ML	Mon Jun 20 22:14:04 2005 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Histories of proof states, with undo / redo and prev / back.
+Histories of proof states, with undo / redo and backtracking.
 *)
 
 signature PROOF_HISTORY =
@@ -28,8 +28,8 @@
 (* datatype proof history *)
 
 type node =
-  Proof.state *			(*first result*)
-  Proof.state Seq.seq; 		(*alternative results*)
+  Proof.state *                 (*first result*)
+  Proof.state Seq.seq;          (*alternative results*)
 
 type proof = node * node list;
 
@@ -55,15 +55,15 @@
 
 (* backtrack *)
 
-fun back_fun recur ((_, stq), nodes) =
+fun backtrack recur ((_, stq), nodes) =
   (case Seq.pull stq of
     NONE =>
       if recur andalso not (null nodes) then
-        (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
+        (writeln "back: trying previous proof state ..."; backtrack recur (hd nodes, tl nodes))
       else raise FAIL "back: no alternatives"
   | SOME result => (result, nodes));
 
-val back = hist_app o back_fun;
+val back = hist_app o backtrack;
 
 
 (* apply transformer *)
diff -r f66ab8a4e98f -r e10b0d5fa33a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jun 20 22:14:03 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jun 20 22:14:04 2005 +0200
@@ -7,8 +7,7 @@
 
 signature TOPLEVEL =
 sig
-  datatype node = Theory of theory | Proof of ProofHistory.T
-    | SkipProof of int History.T * theory
+  datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
   type state
   val toplevel: state
   val is_toplevel: state -> bool
@@ -228,8 +227,7 @@
       end;
 
 fun check_stale state =
-  if not (is_stale state) then ()
-  else warning "Stale theory encountered!";
+  conditional (is_stale state) (fn () => warning "Stale theory encountered!");
 
 end;
 
diff -r f66ab8a4e98f -r e10b0d5fa33a src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Jun 20 22:14:03 2005 +0200
+++ b/src/Pure/display.ML	Mon Jun 20 22:14:04 2005 +0200
@@ -261,7 +261,7 @@
   | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
 
-fun sort_idxs vs = map (apsnd (sort (prod_ord String.compare Int.compare))) vs;
+fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
 fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
 
 fun consts_of t = sort_cnsts (add_consts (t, []));