src/Pure/Isar/proof.ML

 
 
 fun put_data kind f = map_context o ProofContext.put_data kind f;
 val declare_term = map_context o ProofContext.declare_term;
 val add_binds = map_context o ProofContext.add_binds_i;
+val auto_bind_goal = map_context o ProofContext.auto_bind_goal;
+val auto_bind_facts = map_context o ProofContext.auto_bind_facts;
 val put_thms = map_context o ProofContext.put_thms;
 val put_thmss = map_context o ProofContext.put_thmss;
 
 
 (* bind statements *)
 
+(* FIXME
 fun bind_props bs state =
-  let val mk_bind = map (fn (x, t) => ((Syntax.binding x, 0), t)) o ObjectLogic.dest_statement
-  in state |> add_binds (flat (map mk_bind bs)) end;
+  state |> add_binds (flat (map ObjectLogic.statement_bindings bs)) end;
 
 fun bind_thms (name, thms) state =
   let
     val props = map (#prop o Thm.rep_thm) thms;
     val named_props =

 
 fun let_thms name_thms state =
   state
   |> put_thms name_thms
   |> bind_thms name_thms;
+*)
+
+(* FIXME elim (!?) *)
+
+fun let_thms name_thms state =
+  state
+  |> put_thms name_thms;
 
 
 (* facts *)
 
 fun the_facts (State ({facts = Some facts, ...}, _)) = facts

     thm
     |> Drule.forall_intr_list frees
     |> Drule.forall_elim_vars (maxidx + 1)
   end;
 
+fun varify_tfrees thm =
+  let
+    val {hyps, prop, ...} = Thm.rep_thm thm;
+    val frees = foldr Term.add_term_frees (prop :: hyps, []);
+    val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
+  in thm |> Thm.varifyT' leave_tfrees end;
+
 fun implies_elim_hyps thm =
   foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));
 
 fun prep_result state asms t raw_thm =
   let

     val thm =
       raw_thm RS Drule.rev_triv_goal
       |> implies_elim_hyps
       |> Drule.implies_intr_list asms
       |> varify_frees (ProofContext.fixed_names ctxt)
-      |> Thm.varifyT;
+      |> varify_tfrees;
 
     val {hyps, prop, sign, ...} = Thm.rep_thm thm;
     val tsig = Sign.tsig_of sign;
   in
 (* FIXME

 *)
     if not (null hyps) then
       err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
 (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
       err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
-    else thm
+    else (thm, prop)
   end;
 
 
 (* prepare final result *)
 

     val cprop = cterm_of prop;
     val thm = Drule.mk_triv_goal cprop;
   in
     state'
     |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, prop), ([], thm)))
-    |> bind_props [("thesis", prop)]
+    |> auto_bind_goal prop
     |> (if is_chain state then use_facts else reset_facts)
     |> new_block
     |> enter_backward
   end;
 

 (* local_qed *)
 
 fun finish_local print_result state =
   let
     val ((kind, name, asms, t), (_, raw_thm)) = current_goal state;
-    val result = prep_result state asms t raw_thm;
+    val (result, result_prop) = prep_result state asms t raw_thm;
     val (atts, opt_solve) =
       (case kind of
         Goal atts => (atts, solve_goal result)
       | Aux atts => (atts, Seq.single)
       | _ => raise STATE ("No local goal!", state));
   in
     print_result {kind = kind_name kind, name = name, thm = result};
     state
     |> close_block
+    |> auto_bind_facts [result_prop]
     |> have_thmss name atts [Thm.no_attributes [result]]
     |> opt_solve
   end;
 
 fun local_qed finalize print_result state =

 (* global_qed *)
 
 fun finish_global alt_name alt_atts state =
   let
     val ((kind, def_name, asms, t), (_, raw_thm)) = current_goal state;
-    val result = final_result state (prep_result state asms t raw_thm);
+    val result = final_result state (#1 (prep_result state asms t raw_thm));
 
     val name = if_none alt_name def_name;
     val atts =
       (case kind of
         Theorem atts => if_none alt_atts atts