| changeset 69605 | a96320074298 |
| parent 69593 | 3dda49e08b9d |
| child 69661 | a03a63b81f44 |
--- a/src/HOL/Fun.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Fun.thy Sun Jan 06 15:04:34 2019 +0100 @@ -886,7 +886,7 @@ subsubsection \<open>Functorial structure of types\<close> -ML_file "Tools/functor.ML" +ML_file \<open>Tools/functor.ML\<close> functor map_fun: map_fun by (simp_all add: fun_eq_iff)