src/Pure/Isar/class.ML
changeset 60337 c7ca6bb006b0
parent 60249 09377954133b
child 60338 a808b57d5b0d
     1.1 --- a/src/Pure/Isar/class.ML	Mon Jun 01 18:07:36 2015 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jun 01 18:59:19 2015 +0200
     1.3 @@ -336,7 +336,7 @@
     1.4      val rhs2 = Morphism.term phi2 rhs;
     1.5    in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
     1.6  
     1.7 -fun target_const class phi0 prmode ((b, _), rhs) =
     1.8 +fun target_const class phi0 prmode (b, rhs) =
     1.9    let
    1.10      val guess_identity = guess_morphism_identity (b, rhs) Morphism.identity;
    1.11      val guess_canonical = guess_morphism_identity (b, rhs) phi0;
    1.12 @@ -404,7 +404,7 @@
    1.13      val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
    1.14    in
    1.15      lthy
    1.16 -    |> target_const class phi Syntax.mode_default ((b, mx), lhs)
    1.17 +    |> target_const class phi Syntax.mode_default (b, lhs)
    1.18      |> Local_Theory.raw_theory (canonical_const class phi dangling_params
    1.19           ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
    1.20      |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
    1.21 @@ -418,7 +418,7 @@
    1.22      val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
    1.23    in
    1.24      lthy
    1.25 -    |> target_const class phi prmode ((b, mx), lhs)
    1.26 +    |> target_const class phi prmode (b, lhs)
    1.27      |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params
    1.28           ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs'))
    1.29      |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)