src/Pure/Isar/class.ML
changeset 24766 d0de4e48b526
parent 24748 ee0a0eb6b738
child 24770 695a8e087b9f
     1.1 --- a/src/Pure/Isar/class.ML	Sat Sep 29 21:39:50 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Sep 29 21:39:51 2007 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4      val ty = Sign.the_const_constraint thy c;
     1.5    in
     1.6      thy
     1.7 -    |> Sign.add_const_constraint_i (c, NONE)
     1.8 +    |> Sign.add_const_constraint (c, NONE)
     1.9      |> pair (c, Logic.unvarifyT ty)
    1.10    end;
    1.11  
    1.12 @@ -295,7 +295,7 @@
    1.13      val (defs, other_cs) = read_defs raw_defs cs
    1.14        (fold Sign.primitive_arity arities (Theory.copy theory));
    1.15      fun after_qed' cs defs =
    1.16 -      fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
    1.17 +      fold Sign.add_const_constraint (map (apsnd SOME) cs)
    1.18        #> after_qed defs;
    1.19    in
    1.20      theory
    1.21 @@ -570,7 +570,7 @@
    1.22      TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt))
    1.23       (Syntax.check_typs ctxt)
    1.24        (default_typ ctxt constraints) (K NONE)
    1.25 -      (Variable.names_of ctxt) true (map (rpair dummyT) ts)
    1.26 +      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) (SOME true) (map (rpair dummyT) ts)
    1.27      |> #1 |> map #1
    1.28    handle TYPE (msg, _, _) => error msg
    1.29  
    1.30 @@ -618,9 +618,9 @@
    1.31      ctxt
    1.32      |> remove_constraints sort
    1.33      ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort)))
    1.34 -    ||> Context.proof_map (Syntax.add_typ_check typ_check)
    1.35 +    ||> Context.proof_map (Syntax.add_typ_check 0 "class" typ_check)
    1.36      |-> (fn constraints =>
    1.37 -        Context.proof_map (Syntax.add_term_check (term_check constraints)))
    1.38 +        Context.proof_map (Syntax.add_term_check 0 "class" (term_check constraints)))
    1.39    end;
    1.40  
    1.41  val init_ref = ref (K I : sort -> Proof.context -> Proof.context);
    1.42 @@ -793,7 +793,7 @@
    1.43      |> Sign.sticky_prefix prfx
    1.44      |> PureThy.add_defs_i false [(def, [])]
    1.45      |-> (fn [def] => interpret def)
    1.46 -    |> Sign.add_const_constraint_i (c', SOME ty'')
    1.47 +    |> Sign.add_const_constraint (c', SOME ty'')
    1.48      |> Sign.restore_naming thy
    1.49    end;
    1.50