| changeset 59582 | 0fbed69ff081 |
| parent 59058 | a78612c67ec0 |
| child 59621 | 291934bac95e |
--- a/src/HOL/HOLCF/Tools/fixrec.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Wed Mar 04 19:53:18 2015 +0100 @@ -100,7 +100,7 @@ | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]) val lhs_name = - name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of + name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of in