src/Pure/Isar/theory_target.ML
changeset 31869 01fed718958c
parent 30761 ac7570d80c3d
child 31977 e03059ae2d82
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Jun 29 16:17:56 2009 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Jun 29 16:17:57 2009 +0200
     1.3 @@ -330,15 +330,6 @@
     1.4         else I)}
     1.5  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
     1.6  
     1.7 -fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
     1.8 -  let
     1.9 -    val all_arities = map (fn raw_tyco => Sign.read_arity thy
    1.10 -      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    1.11 -    val tycos = map #1 all_arities;
    1.12 -    val (_, sorts, sort) = hd all_arities;
    1.13 -    val vs = Name.names Name.context Name.aT sorts;
    1.14 -  in (tycos, vs, sort) end;
    1.15 -
    1.16  fun gen_overloading prep_const raw_ops thy =
    1.17    let
    1.18      val ctxt = ProofContext.init thy;
    1.19 @@ -356,7 +347,7 @@
    1.20  
    1.21  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
    1.22  fun instantiation_cmd raw_arities thy =
    1.23 -  instantiation (read_multi_arity thy raw_arities) thy;
    1.24 +  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
    1.25  
    1.26  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
    1.27  val overloading_cmd = gen_overloading Syntax.read_term;