src/HOL/Tools/Lifting/lifting_def.ML
changeset 56245 84fc7dfa3cd4
parent 55945 e96383acecf9
child 56518 beb3b6851665
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -547,11 +547,11 @@
     1.4  
     1.5  fun rename_to_tnames ctxt term =
     1.6    let
     1.7 -    fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t
     1.8 +    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
     1.9        | all_typs _ = []
    1.10  
    1.11 -    fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) = 
    1.12 -        (Const ("all", T1) $ Abs (new_name, T2, rename t names)) 
    1.13 +    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
    1.14 +        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
    1.15        | rename t _ = t
    1.16  
    1.17      val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt