src/ZF/Tools/typechk.ML
changeset 30722 623d4831c8cf
parent 30541 9f168bdc468a
child 32091 30e2ffbba718
     1.1 --- a/src/ZF/Tools/typechk.ML	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/ZF/Tools/typechk.ML	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -109,11 +109,13 @@
     1.4  
     1.5  (* concrete syntax *)
     1.6  
     1.7 -val typecheck_meth =
     1.8 -  Method.sections
     1.9 -    [Args.add -- Args.colon >> K (I, TC_add),
    1.10 -     Args.del -- Args.colon >> K (I, TC_del)]
    1.11 -  >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
    1.12 +val typecheck_setup =
    1.13 +  Method.setup @{binding typecheck}
    1.14 +    (Method.sections
    1.15 +      [Args.add -- Args.colon >> K (I, TC_add),
    1.16 +       Args.del -- Args.colon >> K (I, TC_del)]
    1.17 +      >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))))
    1.18 +    "ZF type-checking";
    1.19  
    1.20  val _ =
    1.21    OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
    1.22 @@ -125,7 +127,7 @@
    1.23  
    1.24  val setup =
    1.25    Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
    1.26 -  Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
    1.27 +  typecheck_setup #>
    1.28    Simplifier.map_simpset (fn ss => ss setSolver type_solver);
    1.29  
    1.30  end;