# HG changeset patch
# User wenzelm
# Date 1152031198 -7200
# Node ID 7f841a2b431ccdbe5ff71badb7cf0257e7c39114
# Parent  669a1a6095440e8ab1b7049912a54298f6959c95
added schematic_goal;

diff -r 669a1a609544 -r 7f841a2b431c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jul 04 18:39:57 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 04 18:39:58 2006 +0200
@@ -31,6 +31,7 @@
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val get_goal: state -> context * (thm list * thm)
+  val schematic_goal: state -> bool
   val show_main_goal: bool ref
   val verbose: bool ref
   val pretty_state: int -> state -> Pretty.T list
@@ -306,6 +307,13 @@
   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   in (ctxt, (using, goal)) end;
 
+fun schematic_goal state =
+  let
+    val (_, (_, {statement = (_, propss), ...})) = find_goal state;
+    val tvars = fold (fold Term.add_tvars) propss [];
+    val vars = fold (fold Term.add_vars) propss [];
+  in not (null tvars andalso null vars) end;
+
 
 
 (** pretty_state **)