changeset 39159 | 0dec18004e75 |
parent 38864 | 4abe644fcea5 |
child 39557 | fe5722fce758 |
--- a/src/HOL/Import/shuffler.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Import/shuffler.ML Mon Sep 06 19:13:10 2010 +0200 @@ -346,7 +346,7 @@ fun beta_fun thy assume t = SOME (Thm.beta_conversion true (cterm_of thy t)) -val meta_sym_rew = thm "refl" +val meta_sym_rew = @{thm refl} fun equals_fun thy assume t = case t of