# HG changeset patch
# User wenzelm
# Date 1258399382 -3600
# Node ID d15212c7501c94acdcfd1c63ba63638bdbcbb079
# Parent  474ebcc348e6c35a378afc8f2c602ac7038801d8# Parent  5249bbca5fab28d58959f66f6750a667dba5ba1a
merged

diff -r 474ebcc348e6 -r d15212c7501c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Nov 16 18:33:12 2009 +0000
+++ b/src/HOL/Tools/record.ML	Mon Nov 16 20:23:02 2009 +0100
@@ -1009,14 +1009,20 @@
 (** record simprocs **)
 
 fun future_forward_prf_standard thy prf prop () =
-   let val thm = if !quick_and_dirty then Skip_Proof.make_thm thy prop 
-                 else Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop;
-   in Drule.standard thm end;
+  let val thm =
+    if ! quick_and_dirty then Skip_Proof.make_thm thy prop
+    else if Goal.future_enabled () then
+      Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
+    else prf ()
+  in Drule.standard thm end;
 
 fun prove_common immediate stndrd thy asms prop tac =
-  let val prv = if !quick_and_dirty then Skip_Proof.prove 
-                else if immediate then Goal.prove else Goal.prove_future;
-      val prf = prv (ProofContext.init thy) [] asms prop tac
+  let
+    val prv =
+      if ! quick_and_dirty then Skip_Proof.prove
+      else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
+      else Goal.prove_future;
+    val prf = prv (ProofContext.init thy) [] asms prop tac;
   in if stndrd then Drule.standard prf else prf end;
 
 val prove_future_global = prove_common false;
diff -r 474ebcc348e6 -r d15212c7501c src/Pure/defs.ML
--- a/src/Pure/defs.ML	Mon Nov 16 18:33:12 2009 +0000
+++ b/src/Pure/defs.ML	Mon Nov 16 20:23:02 2009 +0100
@@ -10,10 +10,10 @@
   val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
-  val all_specifications_of: T -> (string * {def: string option, description: string,
-    lhs: typ list, rhs: (string * typ list) list} list) list
-  val specifications_of: T -> string -> {def: string option, description: string,
-    lhs: typ list, rhs: (string * typ list) list} list
+  type spec =
+    {def: string option, description: string, lhs: typ list, rhs: (string * typ list) list}
+  val all_specifications_of: T -> (string * spec list) list
+  val specifications_of: T -> string -> spec list
   val dest: T ->
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
diff -r 474ebcc348e6 -r d15212c7501c src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Nov 16 18:33:12 2009 +0000
+++ b/src/Pure/more_thm.ML	Mon Nov 16 20:23:02 2009 +0100
@@ -75,9 +75,6 @@
   val untag_rule: string -> thm -> thm
   val tag: Properties.property -> attribute
   val untag: string -> attribute
-  val position_of: thm -> Position.T
-  val default_position: Position.T -> thm -> thm
-  val default_position_of: thm -> thm -> thm
   val def_name: string -> string
   val def_name_optional: string -> string -> string
   val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
@@ -380,14 +377,6 @@
 fun untag s x = rule_attribute (K (untag_rule s)) x;
 
 
-(* position *)
-
-val position_of = Position.of_properties o Thm.get_tags;
-
-fun default_position pos = Thm.map_tags (Position.default_properties pos);
-val default_position_of = default_position o position_of;
-
-
 (* def_name *)
 
 fun def_name c = c ^ "_def";