src/Pure/Isar/proof.ML
changeset 7665 1ab0c74cd748
parent 7632 25a0d2ba3a87
child 7669 fcd9c2050836
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Sep 30 21:21:04 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Sep 30 21:21:52 1999 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val sign_of: state -> Sign.sg
     1.5    val reset_thms: string -> state -> state
     1.6    val the_facts: state -> thm list
     1.7 -  val get_goal: state -> thm list * thm
     1.8 +  val get_goal: state -> term * (thm list * thm)
     1.9    val goal_facts: (state -> thm list) -> state -> state
    1.10    val use_facts: state -> state
    1.11    val reset_facts: state -> state
    1.12 @@ -42,7 +42,7 @@
    1.13      (thm list * context attribute list) list -> state -> state
    1.14    val simple_have_thms: string -> thm list -> state -> state
    1.15    val fix: (string list * string option) list -> state -> state
    1.16 -  val fix_i: (string list * typ) list -> state -> state
    1.17 +  val fix_i: (string list * typ option) list -> state -> state
    1.18    val assm: (int -> tactic) * (int -> tactic)
    1.19      -> (string * context attribute list * (string * (string list * string list)) list) list
    1.20      -> state -> state
    1.21 @@ -222,8 +222,8 @@
    1.22    | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state;
    1.23  
    1.24  fun get_goal state =
    1.25 -  let val (_, (_, ((_, goal), _))) = find_goal 0 state
    1.26 -  in goal end;
    1.27 +  let val (_, (_, (((_, _, t), goal), _))) = find_goal 0 state
    1.28 +  in (t, goal) end;
    1.29  
    1.30  fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
    1.31