1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Tue Aug 31 15:36:57 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Tue Aug 31 16:00:13 2010 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4    Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
     1.5        erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
     1.6        rules = (*8.01: copied from*)
     1.7 -      [Thm ("refl", num_str refl),       (*'a<>b -> FALSE' by fun eval_equal*)
     1.8 +      [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
     1.9         Thm ("o_apply", num_str @{thm o_apply}),
    1.10  
    1.11         Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)