src/Pure/Syntax/syn_ext.ML
changeset 32785 ec5292653aff
parent 30189 3633f560f4c3
child 33037 b22e44496dc2
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Sep 30 22:20:58 2009 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Sep 30 22:24:57 2009 +0200
     1.3 @@ -270,9 +270,9 @@
     1.4      fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
     1.5        | rem_pri sym = sym;
     1.6  
     1.7 -    fun logify_types copy_prod (a as (Argument (s, p))) =
     1.8 +    fun logify_types (a as (Argument (s, p))) =
     1.9            if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
    1.10 -      | logify_types _ a = a;
    1.11 +      | logify_types a = a;
    1.12  
    1.13  
    1.14      val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
    1.15 @@ -305,7 +305,7 @@
    1.16        if convert andalso not copy_prod then
    1.17         (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
    1.18        else lhs;
    1.19 -    val symbs' = map (logify_types copy_prod) symbs;
    1.20 +    val symbs' = map logify_types symbs;
    1.21      val xprod = XProd (lhs', symbs', const', pri);
    1.22  
    1.23      val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');