changeset 52456 | 960202346d0c |
parent 52384 | 80c00a851de5 |
child 52467 | 24c6ddb48cb8 |
--- a/src/HOL/Tools/Function/function_core.ML Wed Jun 26 09:58:39 2013 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Wed Jun 26 11:54:45 2013 +0200 @@ -425,7 +425,7 @@ val goalstate = Conjunction.intr graph_is_function complete |> Thm.close_derivation - |> Goal.protect + |> Goal.protect 0 |> fold_rev (Thm.implies_intr o cprop_of) compat |> Thm.implies_intr (cprop_of complete) in