| changeset 55543 | f0ef75c6c0d8 |
| parent 52023 | b477be38a7bb |
| child 58823 | 513268cb2178 |
--- a/src/HOL/Predicate_Compile.thy Mon Feb 17 14:59:09 2014 +0100 +++ b/src/HOL/Predicate_Compile.thy Mon Feb 17 17:49:29 2014 +0100 @@ -81,6 +81,7 @@ Core_Data.PredData.map (Graph.new_node (@{const_name contains}, Core_Data.PredData { + pos = Position.thread_data (), intros = [(NONE, @{thm containsI})], elim = SOME @{thm containsE}, preprocessed = true,