src/Tools/induct.ML
changeset 56245 84fc7dfa3cd4
parent 56231 b98813774a63
child 56334 6b3739fee456
     1.1 --- a/src/Tools/induct.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Tools/induct.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
     1.5  
     1.6  val rearrange_eqs_simproc =
     1.7 -  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
     1.8 +  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
     1.9      (fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));
    1.10  
    1.11  
    1.12 @@ -644,14 +644,16 @@
    1.13  
    1.14  local
    1.15  
    1.16 -fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
    1.17 +fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) =
    1.18 +      c $ Abs (a, T, goal_prefix k B)
    1.19    | goal_prefix 0 _ = Term.dummy_prop
    1.20 -  | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
    1.21 +  | goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) =
    1.22 +      c $ A $ goal_prefix (k - 1) B
    1.23    | goal_prefix _ _ = Term.dummy_prop;
    1.24  
    1.25 -fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
    1.26 +fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1
    1.27    | goal_params 0 _ = 0
    1.28 -  | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
    1.29 +  | goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k - 1) B
    1.30    | goal_params _ _ = 0;
    1.31  
    1.32  fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
    1.33 @@ -670,11 +672,13 @@
    1.34            [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
    1.35             (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
    1.36  
    1.37 -    fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
    1.38 +    fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
    1.39 +          goal_concl k ((a, T) :: xs) B
    1.40        | goal_concl 0 xs B =
    1.41            if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
    1.42            else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
    1.43 -      | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
    1.44 +      | goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) =
    1.45 +          goal_concl (k - 1) xs B
    1.46        | goal_concl _ _ _ = NONE;
    1.47    in
    1.48      (case goal_concl n [] goal of