--- a/src/Pure/Isar/obtain.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Jun 23 11:01:14 2016 +0200
@@ -228,7 +228,7 @@
|> Proof.have true NONE after_qed
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
- [(Thm.empty_binding, [(thesis, [])])] int
+ [(Binding.empty_atts, [(thesis, [])])] int
|-> Proof.refine_insert
|> Proof.map_context (fold Variable.bind_term binds')
end;
@@ -376,7 +376,7 @@
|> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
(obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
- [] [] [(Thm.empty_binding, asms)])
+ [] [] [(Binding.empty_atts, asms)])
|> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
end;
@@ -403,7 +403,7 @@
|> Proof.chain_facts chain_facts
|> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
(SOME before_qed) after_qed
- [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
+ [] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])]
|> snd
|> Proof.refine_singleton
(Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))