| changeset 66125 | 28e782dd0278 |
| parent 66024 | 77d9334830ec |
| child 66126 | 60bf6934fabd |
--- a/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 @@ -165,6 +165,7 @@ fun case_consts_of (Constructors (_, case_consts)) = case_consts | case_consts_of (Abstractor _) = []; + (* functions *) datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy