# HG changeset patch
# User wenzelm
# Date 1149638491 -7200
# Node ID 396dd23c54ef84e0b5a8185e834ab82e441e2667
# Parent  79161b3396916fadd11a980c51617d143d6beeac
added facts_of;
tuned interfaces;

diff -r 79161b339691 -r 396dd23c54ef src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Jun 07 02:01:30 2006 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jun 07 02:01:31 2006 +0200
@@ -26,12 +26,13 @@
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
-  val params_of: ('typ, 'term, 'fact) ctxt -> (string * 'typ) list
-  val prems_of: ('typ, 'term, 'fact) ctxt -> 'term list
+  val params_of: context_i -> (string * typ) list
+  val prems_of: context_i -> term list
+  val facts_of: theory -> context_i ->
+    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
-
   type witness
   val map_witness: (term * thm -> term * thm) -> witness -> witness
   val witness_prop: witness -> term
@@ -41,8 +42,7 @@
   val conclude_witness: witness -> thm
   val mark_witness: term -> term
   val make_witness: term -> thm -> witness
-  val refine_witness: Proof.state -> Proof.state
-
+  val refine_witness: Proof.state -> Proof.state Seq.seq
   val rename: (string * (string * mixfix option)) list -> string -> string
   val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
   val rename_term: (string * (string * mixfix option)) list -> term -> term
@@ -105,6 +105,9 @@
   {name = I, var = I, typ = typ, term = term, fact = map thm,
     attrib = Args.map_values I typ term thm};
 
+
+(* logical content *)
+
 fun params_of (Fixes fixes) = fixes |> map
     (fn (x, SOME T, _) => (x, T)
       | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote x, []))
@@ -114,6 +117,13 @@
   | prems_of (Defines defs) = map (fst o snd) defs
   | prems_of _ = [];
 
+fun assume thy t = Goal.norm_hhf (Thm.assume (Thm.cterm_of thy t));
+
+fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
+  | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
+  | facts_of _ (Notes facts) = facts
+  | facts_of _ _ = [];
+
 
 
 (** pretty printing **)
@@ -276,8 +286,7 @@
   Proof.refine (Method.Basic (K (Method.RAW_METHOD
     (K (ALLGOALS
       (PRECISE_CONJUNCTS ~1 (ALLGOALS
-        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))))
-  #> Seq.hd;
+        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))));
 
 
 (* derived rules *)