| changeset 69597 | ff784d5a5bfb |
| parent 68386 | 98cf1c823c48 |
| child 74224 | e04ec2b9ed97 |
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Sat Jan 05 17:24:33 2019 +0100 @@ -1152,7 +1152,7 @@ by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) ML \<open> -fun dest_fsetT (Type (@{type_name fset}, [T])) = T +fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); \<close>