src/HOL/Tools/Lifting/lifting_term.ML
changeset 60239 755e11e2e15d
parent 60222 78fc1b798c61
child 60642 48dd1cefb4ae
     1.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Sun May 03 14:12:10 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Sun May 03 14:35:48 2015 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4         Pretty.str "don't match."])
     1.5    end
     1.6  
     1.7 -fun get_quot_data quotients s =
     1.8 +fun get_quot_data (quotients: quotients) s =
     1.9    case Symtab.lookup quotients s of
    1.10      SOME qdata => qdata
    1.11    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    1.12 @@ -237,7 +237,7 @@
    1.13  type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
    1.14    comp_lift: typ -> thm * 'a -> thm * 'a }
    1.15  
    1.16 -fun prove_schematic_quot_thm actions quotients ctxt (rty, qty) fold_val =
    1.17 +fun prove_schematic_quot_thm (actions: 'a fold_quot_thm) quotients ctxt (rty, qty) fold_val =
    1.18    let
    1.19      fun lifting_step (rty, qty) =
    1.20        let