src/HOL/Predicate_Compile.thy
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,