src/Tools/Code/code_runtime.ML
changeset 67327 89be5a4f514b
parent 65062 dc746d43f40e
child 67328 5ca7bb565ea2
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Jan 02 21:32:14 2018 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Jan 01 20:42:05 2018 +0000
     1.3 @@ -598,16 +598,18 @@
     1.4  
     1.5  
     1.6  fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
     1.7 -  let
     1.8 -    val ((vs, constrs), _) = Code.get_type (Proof_Context.theory_of ctxt) tyco;
     1.9 -    val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
    1.10 -    val cs = map (fn (c, (_, Ts')) =>
    1.11 -      (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
    1.12 -        ---> dT)) constrs;
    1.13 -  in
    1.14 -    union (op =) cs
    1.15 -    #> fold (add_all_constrs ctxt) Ts
    1.16 -  end;
    1.17 +  case Code.get_type (Proof_Context.theory_of ctxt) tyco of
    1.18 +    ((vs, constrs), false) =>
    1.19 +      let
    1.20 +        val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
    1.21 +        val cs = map (fn (c, (_, Ts')) =>
    1.22 +          (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
    1.23 +            ---> dT)) constrs;
    1.24 +      in
    1.25 +        union (op =) cs
    1.26 +        #> fold (add_all_constrs ctxt) Ts
    1.27 +      end
    1.28 +  | (_, true) => I;
    1.29  
    1.30  fun prep_spec ctxt (raw_ts, raw_dTs) =
    1.31    let