src/HOLCF/IOA/meta_theory/CompoScheds.thy
changeset 39159 0dec18004e75
parent 35215 a03462cbf86f
child 39302 d7728f65b353
     1.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -289,9 +289,9 @@
     1.4  ML {*
     1.5  
     1.6  local
     1.7 -  val defs = [thm "Filter_def", thm "Forall_def", thm "sforall_def", thm "mkex_def",
     1.8 -    thm "stutter_def"]
     1.9 -  val asigs = [thm "asig_of_par", thm "actions_asig_comp"]
    1.10 +  val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
    1.11 +    @{thm stutter_def}]
    1.12 +  val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}]
    1.13  in
    1.14  
    1.15  fun mkex_induct_tac ctxt sch exA exB =