avoid polyeq;
authorwenzelm
Fri Jul 01 22:35:41 2005 +0200 (2005-07-01)
changeset 16668fdb4992cf1d2
parent 16667 f56080acd176
child 16669 4748b1adad9c
avoid polyeq;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/parser.ML
src/Pure/pattern.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jul 01 22:35:20 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jul 01 22:35:41 2005 +0200
     1.3 @@ -1220,7 +1220,7 @@
     1.4      else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
     1.5    end;
     1.6  
     1.7 -fun rem_case name = remove (fn (x, (y, _)) => x = y) name;
     1.8 +fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name;
     1.9  
    1.10  fun add_case ("", _) cases = cases
    1.11    | add_case (name, NONE) cases = rem_case name cases
     2.1 --- a/src/Pure/Syntax/parser.ML	Fri Jul 01 22:35:20 2005 +0200
     2.2 +++ b/src/Pure/Syntax/parser.ML	Fri Jul 01 22:35:41 2005 +0200
     2.3 @@ -627,7 +627,7 @@
     2.4  
     2.5  (*Add parse tree to list and eliminate duplicates
     2.6    saving the maximum precedence*)
     2.7 -fun conc (t, prec:int) [] = (NONE, [(t, prec)])
     2.8 +fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)])
     2.9    | conc (t, prec) ((t', prec') :: ts) =
    2.10        if t = t' then
    2.11          (SOME prec', if prec' >= prec then (t', prec') :: ts
    2.12 @@ -637,7 +637,7 @@
    2.13          in (n, (t', prec') :: ts') end;
    2.14  
    2.15  (*Update entry in used*)
    2.16 -fun update_trees ((B, (i, ts)) :: used) (A, t) =
    2.17 +fun update_trees ((B: nt_tag, (i, ts)) :: used) (A, t) =
    2.18    if A = B then
    2.19      let val (n, ts') = conc t ts
    2.20      in ((A, (i, ts')) :: used, n) end
    2.21 @@ -646,7 +646,7 @@
    2.22      in ((B, (i, ts)) :: used', n) end;
    2.23  
    2.24  (*Replace entry in used*)
    2.25 -fun update_prec (A, prec) used =
    2.26 +fun update_prec (A: nt_tag, prec) used =
    2.27    let fun update ((hd as (B, (_, ts))) :: used, used') =
    2.28          if A = B
    2.29          then used' @ ((A, (prec, ts)) :: used)
     3.1 --- a/src/Pure/pattern.ML	Fri Jul 01 22:35:20 2005 +0200
     3.2 +++ b/src/Pure/pattern.ML	Fri Jul 01 22:35:41 2005 +0200
     3.3 @@ -111,7 +111,7 @@
     3.4      in mpb 0 end;
     3.5  
     3.6  fun idx [] j     = raise Unif
     3.7 -  | idx(i::is) j = if i=j then length is else idx is j;
     3.8 +  | idx(i::is) j = if (i:int) =j then length is else idx is j;
     3.9  
    3.10  fun at xs i = List.nth (xs,i);
    3.11  
    3.12 @@ -202,7 +202,7 @@
    3.13  (* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *)
    3.14  fun mk_ff_list(is,js) =
    3.15      let fun mk([],[],_)        = []
    3.16 -          | mk(i::is,j::js, k) = if i=j then k :: mk(is,js,k-1)
    3.17 +          | mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1)
    3.18                                          else mk(is,js,k-1)
    3.19            | mk _               = error"mk_ff_list"
    3.20      in mk(is,js,length is-1) end;
    3.21 @@ -408,8 +408,8 @@
    3.22      let val (ph,pargs) = strip_comb pat
    3.23          fun rigrig1(iTs,oargs) =
    3.24                Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
    3.25 -        fun rigrig2((a,Ta),(b,Tb),oargs) =
    3.26 -              if a<> b then raise MATCH
    3.27 +        fun rigrig2((a:string,Ta),(b,Tb),oargs) =
    3.28 +              if a <> b then raise MATCH
    3.29                else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
    3.30      in case ph of
    3.31           Var(ixn,T) =>
     4.1 --- a/src/Pure/type_infer.ML	Fri Jul 01 22:35:20 2005 +0200
     4.2 +++ b/src/Pure/type_infer.ML	Fri Jul 01 22:35:41 2005 +0200
     4.3 @@ -448,7 +448,7 @@
     4.4  
     4.5  fun get_sort tsig def_sort map_sort raw_env =
     4.6    let
     4.7 -    fun eq ((xi, S), (xi', S')) =
     4.8 +    fun eq ((xi: indexname, S), (xi', S')) =
     4.9        xi = xi' andalso Type.eq_sort tsig (S, S');
    4.10  
    4.11      val env = gen_distinct eq (map (apsnd map_sort) raw_env);