changeset 43842 | f035d867fb41 |
parent 43837 | 1183951365de |
child 44058 | ae85c5d64913 |
--- a/src/Pure/Isar/element.ML Fri Jul 15 14:07:12 2011 +0200 +++ b/src/Pure/Isar/element.ML Fri Jul 15 16:51:01 2011 +0200 @@ -526,7 +526,7 @@ fun activate raw_elem ctxt = let val elem = raw_elem |> map_ctxt - {binding = tap (fn b => if Binding.is_empty b then "" else Variable.check_name b), + {binding = I, typ = I, term = I, pattern = I,