src/HOLCF/Tools/pcpodef.ML
changeset 36153 1ac501e16a6a
parent 35994 9cc3df9a606e
child 36241 2a4cec6bcae2
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Thu Apr 15 18:00:21 2010 +0200
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Thu Apr 15 18:09:22 2010 +0200
     1.3 @@ -169,18 +169,18 @@
     1.4      val _ = Theory.requires thy "Pcpodef" "pcpodefs";
     1.5  
     1.6      (*rhs*)
     1.7 -    val (_, tmp_lthy) =
     1.8 -      thy |> Theory.copy |> Theory_Target.init NONE
     1.9 -      |> Typedecl.predeclare_constraints (tname, raw_args, mx);
    1.10 -    val set = prep_term tmp_lthy raw_set;
    1.11 -    val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
    1.12 +    val tmp_ctxt =
    1.13 +      ProofContext.init thy
    1.14 +      |> fold (Variable.declare_typ o TFree) raw_args;
    1.15 +    val set = prep_term tmp_ctxt raw_set;
    1.16 +    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
    1.17  
    1.18      val setT = Term.fastype_of set;
    1.19      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    1.20 -      error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT));
    1.21 +      error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT));
    1.22  
    1.23      (*lhs*)
    1.24 -    val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
    1.25 +    val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args;
    1.26      val full_tname = Sign.full_name thy tname;
    1.27      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.28