| changeset 16121 | a80aa66d2271 |
| parent 15793 | acfdd493f5c4 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/Bali/AxExample.thy Tue May 31 11:53:11 2005 +0200 +++ b/src/HOL/Bali/AxExample.thy Tue May 31 11:53:12 2005 +0200 @@ -39,7 +39,7 @@ declare split_if_asm [split del] declare lvar_def [simp] -ML_setup {* +ML {* fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty; val ax_tac = REPEAT o rtac allI THEN'