# HG changeset patch
# User wenzelm
# Date 938719312 -7200
# Node ID 1ab0c74cd74858b6bf13f76ff3efe770e1355a6f
# Parent  c151ac5955516966aaa9e9a595addd44ea216004
get_goal: prop;
fix_i: typ option;

diff -r c151ac595551 -r 1ab0c74cd748 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Sep 30 21:21:04 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 30 21:21:52 1999 +0200
@@ -17,7 +17,7 @@
   val sign_of: state -> Sign.sg
   val reset_thms: string -> state -> state
   val the_facts: state -> thm list
-  val get_goal: state -> thm list * thm
+  val get_goal: state -> term * (thm list * thm)
   val goal_facts: (state -> thm list) -> state -> state
   val use_facts: state -> state
   val reset_facts: state -> state
@@ -42,7 +42,7 @@
     (thm list * context attribute list) list -> state -> state
   val simple_have_thms: string -> thm list -> state -> state
   val fix: (string list * string option) list -> state -> state
-  val fix_i: (string list * typ) list -> state -> state
+  val fix_i: (string list * typ option) list -> state -> state
   val assm: (int -> tactic) * (int -> tactic)
     -> (string * context attribute list * (string * (string list * string list)) list) list
     -> state -> state
@@ -222,8 +222,8 @@
   | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state;
 
 fun get_goal state =
-  let val (_, (_, ((_, goal), _))) = find_goal 0 state
-  in goal end;
+  let val (_, (_, (((_, _, t), goal), _))) = find_goal 0 state
+  in (t, goal) end;
 
 fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));