src/HOL/Bali/AxExample.thy
changeset 55151 f331472f1027
parent 55143 04448228381d
child 58887 38db8ddc0f57
     1.1 --- a/src/HOL/Bali/AxExample.thy	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Sun Jan 26 13:45:40 2014 +0100
     1.3 @@ -42,8 +42,9 @@
     1.4  
     1.5  ML {*
     1.6  fun inst1_tac ctxt s t xs st =
     1.7 -  case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
     1.8 -  SOME i => instantiate_tac ctxt [((s, i), t)] xs st | NONE => Seq.empty;
     1.9 +  (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
    1.10 +    SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st
    1.11 +  | NONE => Seq.empty);
    1.12  
    1.13  val ax_tac =
    1.14    REPEAT o rtac allI THEN'