changeset 60826 | 695cf1fab6cc |
parent 60752 | b48830b670a1 |
child 62922 | 96691631c1eb |
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 28 21:47:03 2015 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 28 23:14:40 2015 +0200 @@ -20,7 +20,7 @@ | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); fun prf_of thy thm = - Reconstruct.proof_of thm + Reconstruct.proof_of thy thm |> Reconstruct.expand_proof thy [("", NONE)]; (* FIXME *) fun subsets [] = [[]]